anchor.diff:  
   let PART_MATCH,GEN_PART_MATCH =
     let rec match_bvs t1 t2 acc =
  -    try let v1,b1 = dest_abs t1
  -        and v2,b2 = dest_abs t2 in
  -        let n1 = fst(dest_var v1) and n2 = fst(dest_var v2) in
  -        let newacc = if n1 = n2 then acc else insert (n1,n2) acc in
  -        match_bvs b1 b2 newacc
  -    with Failure _ -> try
  +    try 
  +      let v1,b1 = dest_abs t1
  +      let v2,b2 = dest_abs t2
  +      let n1 = fst(dest_var v1) 
  +      let n2 = fst(dest_var v2)
  +      let newacc = 
  +        if n1 = n2 then acc 
  +        else insert (n1,n2) acc
  +      match_bvs b1 b2 newacc
  +    with Failure _ -> 
  +      try
           let l1,r1 = dest_comb t1
  -        and l2,r2 = dest_comb t2 in
  +        let l2,r2 = dest_comb t2
           match_bvs l1 l2 (match_bvs r1 r2 acc)
  -    with Failure _ -> acc in
  +      with Failure _ -> acc
     let PART_MATCH partfn th =
       let sth = SPEC_ALL th in
       let bod = concl sth in
  
positive.code:     let args,lam = funpow n (fun (l,t) -> (rand t)::l,rator t) ([],tm) in
      rev_itlist (fun a l -> let v,b = dest_abs l in vsubst[a,v] b) args lam in
    let rec ho_betas bcs pat tm =
      if is_var pat or is_const pat then fail() else
      try let bv,bod = dest_abs tm in
          mk_abs(bv,ho_betas bcs (body pat) bod)
      with Failure _ ->
  
negative.code: 
  let (term_unify:term list -> term -> term -> instantiation) =
    let augment1 sofar (s,x) =
      let s' = subst sofar s
      if vfree_in x s && not (s = x) then failwith "augment_insts"
      else (s',x)
    let raw_augment_insts p insts =
      p::(map (augment1 [p]) insts)
    let augment_insts(t,v) insts =
      let t' = vsubst insts t
      if t' = v then insts
      elif vfree_in v t' then failwith "augment_insts"
      else raw_augment_insts (t',v) insts
    let rec unify vars tm1 tm2 sofar =
      if tm1 = tm2 then sofar
      elif is_var tm1 && mem tm1 vars then
        try 
          let tm1' = rev_assoc tm1 sofar
          unify vars tm1' tm2 sofar
        with Failure "find" ->
            augment_insts (tm2,tm1) sofar
      elif is_var tm2 && mem tm2 vars then
        try 
           let tm2' = rev_assoc tm2 sofar
           unify vars tm1 tm2' sofar
        with Failure "find" ->
            augment_insts (tm1,tm2) sofar
      elif is_abs tm1 then
        let tm1' = body tm1
        let tm2' = subst [bndvar tm1,bndvar tm2] (body tm2)
        unify vars tm1' tm2' sofar
      else
        let l1,r1 = dest_comb tm1
        let l2,r2 = dest_comb tm2
        unify vars l1 l2 (unify vars r1 r2 sofar)
    fun vars tm1 tm2 -> [],unify vars tm1 tm2 [],[];;
  
  (* ------------------------------------------------------------------------- *)
  