anchor.diff:      (* ----------------------------------------------------------------------- *)
   
       let meson_single_expand loffset rule ((g, ancestors), (insts, offset, size)) = 
  -        let (hyps, conc), tag = rule
  -        let allins = rev_itlist2 (fol_unify loffset) (snd g) (snd conc) insts
  -        let locin, globin = separate_insts offset insts allins
  -        let mk_ihyp h = 
  -            let h' = fol_inst_bump offset locin h
  -            h', checkan insts h' ancestors
  -        let newhyps = map mk_ihyp hyps
  -        inferences := !inferences + 1
  -        newhyps, (globin, offset + offinc, size - length hyps)
  +        choice {
  +            let (hyps, conc), tag = rule
  +            let! allins = Choice.List.foldBack2 (fol_unify loffset) (snd g) (snd conc) insts
  +            let locin, globin = separate_insts offset insts allins
  +            let mk_ihyp h = 
  +                choice {
  +                    let h' = fol_inst_bump offset locin h
  +                    let! fts = checkan insts h' ancestors
  +                    return h', fts
  +                }
  +            let! newhyps = Choice.List.map mk_ihyp hyps
  +            inferences := !inferences + 1
  +            return newhyps, (globin, offset + offinc, size - length hyps)
  +        }
   
       (* ----------------------------------------------------------------------- *)
       (* Perform first basic expansion which allows continuation call.           *)
       (* ----------------------------------------------------------------------- *)
   
       let meson_expand_cont loffset rules state cont = 
  -        // NOTE: wrong use of Some, need to change this
  -        tryfind (fun r -> Some <| cont (snd r) (meson_single_expand loffset r state)) rules
  +        // NOTE: we change cont to return option (the original version throws exceptions)
  +        tryfind (fun r -> cont (snd r) (Choice.get <| meson_single_expand loffset r state)) rules
           |> Option.getOrFailWith "tryfind"
   
       (* ----------------------------------------------------------------------- *)
  
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 t' = (p', a)
          let ourancp, otheranc = remove (fun (pr, _) -> pr = p') ancestors |> Option.fill((p', []), ancestors)
          let ouranc = snd ourancp
          if exists (fun u -> fol_atom_eq insts t' (snd(fst u))) ouranc then 
              Choice.failwith "insertan: loop"
          else 
              Choice.result ((p', (([], t'), (0, TRUTH)) :: ouranc) :: otheranc)
  
      (* ----------------------------------------------------------------------- *)
      (* Apply a multi-level "graph" instantiation.                              *)
  