anchor.diff:  (* Searching for terms.                                                      *)
   (* ------------------------------------------------------------------------- *)
   
  +/// Searches a term for a subterm that satis+es a given predicate.
   let rec find_term p tm = 
       if p tm then tm
       elif is_abs tm then find_term p (body tm)
  
positive.code: (* Syntax for binary operators.                                              *)
  (* ------------------------------------------------------------------------- *)
  
  let is_binop op tm = 
      match tm with
      | Comb(Comb(op', _), _) -> op' = op
      | _ -> false
  
  let dest_binop op tm = 
      match tm with
      | Comb(Comb(op', l), r) when op' = op -> (l, r)
      | _ -> failwith "dest_binop"
  
  let mk_binop op tm1 = 
      let f = mk_comb(op, tm1)
      fun tm2 -> mk_comb(f, tm2)
  
  let list_mk_binop op = end_itlist(mk_binop op)
  let binops op = striplist(dest_binop op)
  (* ------------------------------------------------------------------------- *)
  (* Some common special cases                                                 *)
  (* ------------------------------------------------------------------------- *)
  
  let is_conj = is_binary "/\\"
  let dest_conj = dest_binary "/\\"
  let conjuncts = striplist dest_conj
  let is_imp = is_binary "==>"
  let dest_imp = dest_binary "==>"
  let is_forall = is_binder "!"
  let dest_forall = dest_binder "!"
  let strip_forall = splitlist dest_forall
  let is_exists = is_binder "?"
  let dest_exists = dest_binder "?"
  let strip_exists = splitlist dest_exists
  let is_disj = is_binary "\\/"
  let dest_disj = dest_binary "\\/"
  let disjuncts = striplist dest_disj
  
  let is_neg tm = 
      try 
          fst(dest_const(rator tm)) = "~"
      with
      | Failure _ -> false
  
  let dest_neg tm = 
      try 
          let n, p = dest_comb tm
  
negative.code:         with
          | Failure _ -> failwith "dest_gabs: Not a generalized abstraction"
  
  /// Tests if a term is a basic or generalized abstraction.
  let is_gabs = can dest_gabs
  
  /// Constructs a generalized abstraction.
  let mk_gabs = 
      let mk_forall(v, t) = 
          let cop = mk_const("!", [type_of v, aty])
  