anchor.diff:      (* ----------------------------------------------------------------------- *)
   
       let meson_expand rules ((g, ancestors), ((insts, offset, size) as tup)) cont = 
  -        let pr = fst g
  -        let newancestors = insertan insts g ancestors
  -        let newstate = (g, newancestors), tup
  -        try 
  -            if !meson_prefine && pr > 0
  -            then failwith "meson_expand"
  -            else 
  -                let arules =
  -                    assoc pr ancestors
  -                    |> Option.getOrFailWith "find"
  -                meson_expand_cont 0 arules newstate cont
  -        with
  -        | Cut as e ->
  -            nestedFailwith e "meson_expand"
  -        | Failure _ -> 
  -            try 
  -                let crules = 
  -                    filter (fun ((h, _), _) -> length h <= size) (assoc pr rules |> Option.getOrFailWith "find")
  -                meson_expand_cont offset crules newstate cont
  -            with
  -            | Cut as e ->
  -                nestedFailwith e "meson_expand"
  -            | Failure _ as e ->
  -                nestedFailwith e "meson_expand"
  +        choice { 
  +            let pr = fst g
  +            let! newancestors = insertan insts g ancestors
  +            let newstate = (g, newancestors), tup
  +            let v =
  +                try 
  +                    if !meson_prefine && pr > 0 then 
  +                        failwith "meson_expand"
  +                    else 
  +                        let arules = assoc pr ancestors |> Option.getOrFailWith "find"
  +                        Choice.result <| meson_expand_cont 0 arules newstate cont
  +                with
  +                | Cut as e -> 
  +                    Choice.nestedFailwith e "meson_expand"
  +                | Failure _ -> 
  +                    try 
  +                        let crules = filter (fun ((h, _), _) -> length h <= size) (assoc pr rules |> Option.getOrFailWith "find")
  +                        Choice.result <| meson_expand_cont offset crules newstate cont
  +                    with
  +                    | Cut as e -> 
  +                        Choice.nestedFailwith e "meson_expand"
  +                    | Failure _ as e -> 
  +                        Choice.nestedFailwith e "meson_expand"
  +            return! v 
  +        }
   
       (* ----------------------------------------------------------------------- *)
       (* Simple Prolog engine organizing search and backtracking.                *)
  
positive.code: 
      let expand_goal rules = 
          let rec expand_goal depth ((g, _), (insts, offset, size) as state) cont = 
              if depth < 0
              then failwith "expand_goal: too deep"
              else 
                  meson_expand rules state 
                      (fun apprule (_, (pinsts, _, _) as newstate) -> 
                              expand_goals (depth - 1) newstate 
                                  (cacheconts
                                       (fun (gs, (newinsts, newoffset, newsize)) ->
                                               let locin, globin = 
                                                   separate_insts offset pinsts 
                                                       newinsts
                                               let g' = 
                                                   Subgoal
                                                       (g, gs, apprule, offset, 
                                                        locin)
                                               if globin = insts && gs = []
                                               then 
                                                   try 
                                                       cont
                                                           (g', 
                                                            (globin, newoffset, 
                                                             size))
                                                   with
                                                   | Failure _ -> raise Cut
                                               else 
                                                   try 
                                                       cont
                                                           (g', 
                                                            (globin, newoffset, 
                                                             newsize))
                                                   with
                                                   | Cut as e -> nestedFailwith e "expand_goal"
                                                   | Failure _ as e -> 
                                                       nestedFailwith e "expand_goal")))
  
          and expand_goals depth (gl, (insts, offset, size as tup)) cont = 
              match gl with
              | [] -> cont([], tup)
              | [g] -> 
                  expand_goal depth (g, tup) (fun (g', stup) -> cont([g'], stup))
              | gl -> 
                  if size >= !meson_dcutin
                  then 
                      let lsize = size / (!meson_skew)
                      let rsize = size - lsize
                      let lgoals, rgoals = chop_list (length gl / 2) gl
  
negative.code:         | Fnapp(f, fargs), Fnapp(g, gargs) -> 
              f = g && forall2 (fol_eq insts) fargs gargs
          | _, Fvar(x) -> 
              match rev_assoc x insts with
              | Some tm2' ->
                   fol_eq insts tm1 tm2'
              | None -> 
                   istriv insts x tm1
                   |> Choice.fill false
  
          | Fvar(x), _ -> 
              match rev_assoc x insts with
              | Some tm1' ->
                   fol_eq insts tm1' tm2
              | None -> 
                   istriv insts x tm2
                   |> Choice.fill false
  
      let fol_atom_eq insts (p1, args1) (p2, args2) = 
          p1 = p2 && forall2 (fol_eq insts) args1 args2
  