anchor.diff:  (* Instantiates types for constant c and iteratively makes combination.      *)
   (* ------------------------------------------------------------------------- *)
   
  +/// Applies constant to list of arguments, instantiating constant type as needed.
   let list_mk_icomb cname args = 
       let atys, _ = nsplit dest_fun_ty args (get_const_type cname)
       let tyin = itlist2 (fun g a -> type_match g (type_of a)) atys args []
  
positive.code: (* Alpha conversion term operation.                                          *)
  (* ------------------------------------------------------------------------- *)
  
  let alpha v tm = 
      let v0, bod = 
          try 
  
negative.code: (* Free variables in assumption list and conclusion of a theorem.            *)
  (* ------------------------------------------------------------------------- *)
  
  /// Returns a list of the variables free in a theorem's assumptions and conclusion.
  let thm_frees th = 
      let asl, c = dest_thm th
      itlist (union << frees) asl (frees c)
  