anchor.diff:      let rec fol_subst_partial insts tm = 
           match tm with
           | Fvar(v) -> 
  -            (try 
  -                 let t =
  -                    rev_assoc v insts
  -                    |> Option.getOrFailWith "find"
  -                 fol_subst_partial insts t
  -             with
  -             | Failure "find" -> tm)
  -        | Fnapp(f, args) -> Fnapp(f, map (fol_subst_partial insts) args)
  +            match rev_assoc v insts with
  +            | Some t ->
  +                 fol_subst_partial insts t             
  +            | None -> tm
  +        | Fnapp(f, args) -> 
  +            Fnapp(f, map (fol_subst_partial insts) args)
   
       (* ----------------------------------------------------------------------- *)
       (* Tease apart local and global instantiations.                            *)
  
positive.code:     (* ----------------------------------------------------------------------- *)
  
      let separate_insts offset oldinsts newinsts = 
          let locins, globins = 
              qpartition (fun (_, v) -> offset <= v) oldinsts newinsts
          if globins = oldinsts
          then 
              map (fun (t, x) -> fol_subst_partial newinsts t, x) locins, oldinsts
          else 
              map (fun (t, x) -> fol_subst_partial newinsts t, x) locins, 
  
negative.code:     let fol_of_hol_clauses = 
          let eqt (a1, (b1, c1)) (a2, (b2, c2)) = 
              ((a1 = a2) && (b1 = b2) && (equals_thm c1 c2))
  
          let mk_negated(p, a) = -p, a
  
          let rec mk_contraposes n th used unused sofar = 
              match unused with
              | [] -> sofar
              | h :: t -> 
                  let nw = (map mk_negated (used @ t), h), (n, th)
                  mk_contraposes (n + 1) th (used @ [h]) t (nw :: sofar)
  
          let fol_of_hol_clause th = 
              let lconsts = freesl(hyp <| Choice.get th)
              let tm = concl <| Choice.get th
              let hlits = disjuncts tm
              let flits = map (Choice.get << fol_of_literal [] lconsts) hlits
              let basics = mk_contraposes 0 th [] flits []
              if forall (fun (p, _) -> p < 0) flits then ((map mk_negated flits, (1, [])), (-1, th)) :: basics
              else basics
  
          fun thms -> 
              let rawrules = itlist (union' eqt << fol_of_hol_clause) thms []
              let prs = setify(map (fst << snd << fst) rawrules)
              let prules = map (fun t -> t, filter ((=) t << fst << snd << fst) rawrules) prs
              let srules = sort (fun (p, _) (q, _) -> abs(p) <= abs(q)) prules
              srules
  
  