anchor.diff:              let l1, r1 = Choice.get <| dest_comb tm1
               let l2, r2 = Choice.get <| dest_comb tm2
               unify vars l1 l2 (unify vars r1 r2 sofar)
  +
       fun vars tm1 tm2 -> 
  -        Choice.attempt (fun () -> [], unify vars tm1 tm2 [], [])
  +        Choice.attempt <| fun () ->
  +            [], unify vars tm1 tm2 [], []
   
   (* ------------------------------------------------------------------------- *)
   (* Modify bound variable names at depth. (Not very efficient...)             *)
  
positive.code: (* ------------------------------------------------------------------------- *)
  
  /// Match one term against another.
  let term_match : term list -> term -> term -> _ = 
      let safe_inserta ((y, x) as n) l = 
          try 
              let z =
                  rev_assoc x l
                  |> Option.getOrFailWith "find"
              if aconv y z
              then l
              else failwith "safe_inserta"
          with
          | Failure "find" -> n :: l
      let safe_insert ((y, x) as n) l = 
          try 
              let z =
                  rev_assoc x l
                  |> Option.getOrFailWith "find"
              if compare y z = 0
              then l
              else failwith "safe_insert"
          with
          | Failure "find" -> n :: l
      let mk_dummy = 
          let name = fst(Choice.get <| dest_var(genvar aty))
          fun ty -> mk_var(name, ty)
      let rec term_pmatch lconsts env vtm ctm ((insts, homs) as sofar) = 
          match (vtm, ctm) with
          | Var(_, _), _ -> 
              try 
                  let ctm' =
                      rev_assoc vtm env
                      |> Option.getOrFailWith "find"
                  if compare ctm' ctm = 0
                  then sofar
                  else failwith "term_pmatch"
              with
              | Failure "find" -> 
                  if mem vtm lconsts
                  then 
                      if compare ctm vtm = 0
                      then sofar
                      else 
                          failwith "term_pmatch: can't instantiate local constant"
                  else safe_inserta (ctm, vtm) insts, homs
          | Const(vname, vty), Const(cname, cty) -> 
              if compare vname cname = 0
              then 
                  if compare vty cty = 0
                  then sofar
                  else safe_insert (mk_dummy cty, mk_dummy vty) insts, homs
              else failwith "term_pmatch"
          | Abs(vv, vbod), Abs(cv, cbod) -> 
              let sofar' = 
                  safe_insert 
                      (mk_dummy(snd(Choice.get <| dest_var cv)), mk_dummy(snd(Choice.get <| dest_var vv))) 
                      insts, homs
              term_pmatch lconsts ((cv, vv) :: env) vbod cbod sofar'
          | _ -> 
              let vhop = repeat (Choice.toOption << rator) vtm
              if is_var vhop && not(mem vhop lconsts) 
                 && (Option.isNone <| rev_assoc vhop env)
              then 
                  let vty = Choice.get <| type_of vtm
                  let cty = Choice.get <| type_of ctm
                  let insts' = 
                      if compare vty cty = 0
                      then insts
                      else safe_insert (mk_dummy cty, mk_dummy vty) insts
                  (insts', (env, ctm, vtm) :: homs)
              else 
                  let lv, rv = Choice.get <| dest_comb vtm
                  let lc, rc = Choice.get <| dest_comb ctm
                  let sofar' = term_pmatch lconsts env lv lc sofar
                  term_pmatch lconsts env rv rc sofar'
      let get_type_insts insts = 
          itlist (fun (t, x) -> Choice.get << type_match (snd(Choice.get <| dest_var x)) (Choice.get <| type_of t)) insts
      let separate_insts insts = 
          let realinsts, patterns = partition (is_var << snd) insts
          let betacounts = 
              if patterns = []
              then []
              else 
                  itlist (fun (_, p) sof -> 
                          let hop, args = strip_comb p
                          try 
                              safe_insert (length args, hop) sof
                          with
                          | Failure _ -> 
                              (warn true 
                                   "Inconsistent patterning in higher order match"
                               sof)) patterns []
          let tyins = get_type_insts realinsts []
          betacounts, mapfilter (fun (t, x) -> 
                              let x' = 
                                  let xn, xty = Choice.get <| dest_var x
                                  mk_var(xn, type_subst tyins xty)
                              if compare t x' = 0
                              then None
                              else Some(t, x')) realinsts, tyins
      let rec term_homatch lconsts tyins (insts, homs) = 
          if homs = []
          then insts
          else 
              let (env, ctm, vtm) = hd homs
              if is_var vtm
              then 
                  if compare ctm vtm = 0
                  then term_homatch lconsts tyins (insts, tl homs)
                  else 
                      let newtyins = 
                          safe_insert (Choice.get <| type_of ctm, snd(Choice.get <| dest_var vtm)) tyins
                      let newinsts = (ctm, vtm) :: insts
                      term_homatch lconsts newtyins (newinsts, tl homs)
              else 
  
negative.code: 
      fun (bcs, tmin, tyin) th -> 
          let ith = 
              if tyin = [] then th
              else INST_TYPE tyin th
          if tmin = [] then ith
          else
              choice { 
                  let tth = INST tmin ith
  