# HG changeset patch
# User paulson
# Date 865510048 -7200
# Node ID 2cccd0e3e9ea7847e160e89803e67d8dd6e903e6
# Parent  91a91790899a1c3904da94f559bdc83a5147a9d0
Numerous simplifications and removal of HOL-isms
Addition of the "simpset" feature (replacing references to \!simpset)

diff -r 91a91790899a -r 2cccd0e3e9ea TFL/dcterm.sml
--- a/TFL/dcterm.sml	Thu Jun 05 13:26:09 1997 +0200
+++ b/TFL/dcterm.sml	Thu Jun 05 13:27:28 1997 +0200
@@ -35,8 +35,6 @@
     val is_let : cterm -> bool
     val is_neg : cterm -> bool
     val is_pair : cterm -> bool
-    val list_mk_abs : cterm list -> cterm -> cterm
-    val list_mk_exists : cterm list * cterm -> cterm
     val list_mk_disj : cterm list -> cterm
     val strip_abs : cterm -> cterm list * cterm
     val strip_comb : cterm -> cterm * cterm list
@@ -57,14 +55,6 @@
 val can = Utils.can;
 fun swap (x,y) = (y,x);
 
-fun itlist f L base_value =
-   let fun it [] = base_value
-         | it (a::rst) = f a (it rst)
-   in it L 
-   end;
-
-val end_itlist = Utils.end_itlist;
-
 
 (*---------------------------------------------------------------------------
  * Some simple constructor functions.
@@ -164,10 +154,7 @@
 (*---------------------------------------------------------------------------
  * Iterated creation.
  *---------------------------------------------------------------------------*)
-val list_mk_abs = itlist cabs;
-
-fun list_mk_exists(V,t) = itlist(fn v => fn b => mk_exists(v, b)) V t;
-val list_mk_disj = end_itlist(fn d1 => fn tm => mk_disj(d1, tm))
+val list_mk_disj = Utils.end_itlist(fn d1 => fn tm => mk_disj(d1, tm))
 
 (*---------------------------------------------------------------------------
  * Iterated destruction. (To the "right" in a term.)
diff -r 91a91790899a -r 2cccd0e3e9ea TFL/post.sml
--- a/TFL/post.sml	Thu Jun 05 13:26:09 1997 +0200
+++ b/TFL/post.sml	Thu Jun 05 13:27:28 1997 +0200
@@ -6,13 +6,6 @@
 Postprocessing of TFL definitions
 *)
 
-(*-------------------------------------------------------------------------
-Three postprocessors are applied to the definition:
-    - a wellfoundedness prover (WF_TAC)
-    - a simplifier (tries to eliminate the language of termination expressions)
-    - a termination prover
-*-------------------------------------------------------------------------*)
-
 signature TFL = 
   sig
    structure Prim : TFL_sig
@@ -20,20 +13,17 @@
    val tgoalw : theory -> thm list -> thm list -> thm list
    val tgoal: theory -> thm list -> thm list
 
-   val WF_TAC : thm list -> tactic
-
-   val simplifier : thm -> thm
-   val std_postprocessor : theory 
+   val std_postprocessor : simpset -> theory 
                            -> {induction:thm, rules:thm, TCs:term list list} 
                            -> {induction:thm, rules:thm, nested_tcs:thm list}
 
    val define_i : theory -> string -> term -> term list
-                  -> theory * (thm * Prim.pattern list)
+                  -> theory * Prim.pattern list
 
    val define   : theory -> string -> string -> string list 
                   -> theory * Prim.pattern list
 
-   val simplify_defn : theory * (string * Prim.pattern list)
+   val simplify_defn : simpset -> theory * (string * Prim.pattern list)
                         -> {rules:thm list, induct:thm, tcs:term list}
 
   (*-------------------------------------------------------------------------
@@ -56,51 +46,38 @@
  * have a tactic directly applied to them.
  *--------------------------------------------------------------------------*)
 fun termination_goals rules = 
-    map (Logic.freeze_vars o HOLogic.dest_Trueprop)
+    map (#1 o Type.freeze_thaw o HOLogic.dest_Trueprop)
       (foldr (fn (th,A) => union_term (prems_of th, A)) (rules, []));
 
- (*---------------------------------------------------------------------------
-  * Finds the termination conditions in (highly massaged) definition and 
-  * puts them into a goalstack.
-  *--------------------------------------------------------------------------*)
- fun tgoalw thy defs rules = 
-    let val L = termination_goals rules
-        open USyntax
-        val g = cterm_of (sign_of thy) (HOLogic.mk_Trueprop(list_mk_conj L))
-    in goalw_cterm defs g
-    end;
+(*---------------------------------------------------------------------------
+ * Finds the termination conditions in (highly massaged) definition and 
+ * puts them into a goalstack.
+ *--------------------------------------------------------------------------*)
+fun tgoalw thy defs rules = 
+   let val L = termination_goals rules
+       open USyntax
+       val g = cterm_of (sign_of thy) (HOLogic.mk_Trueprop(list_mk_conj L))
+   in goalw_cterm defs g
+   end;
 
- fun tgoal thy = tgoalw thy [];
-
- (*---------------------------------------------------------------------------
-  * Simple wellfoundedness prover.
-  *--------------------------------------------------------------------------*)
- fun WF_TAC thms = REPEAT(FIRST1(map rtac thms))
- val WFtac = WF_TAC[wf_measure, wf_inv_image, wf_lex_prod, wf_less_than, 
-                    wf_trancl];
+fun tgoal thy = tgoalw thy [];
 
- val terminator = simp_tac(!simpset addsimps [less_Suc_eq]) 1
-                  THEN TRY(best_tac
-                           (!claset addSDs [not0_implies_Suc]
-                                    addss (!simpset)) 1);
-
- val simpls = [less_eq RS eq_reflection,
-               lex_prod_def, measure_def, inv_image_def];
+(*---------------------------------------------------------------------------
+* Three postprocessors are applied to the definition.  It
+* attempts to prove wellfoundedness of the given relation, simplifies the
+* non-proved termination conditions, and finally attempts to prove the 
+* simplified termination conditions.
+*--------------------------------------------------------------------------*)
+fun std_postprocessor ss =
+  Prim.postprocess
+   {WFtac      = REPEAT (ares_tac [wf_measure, wf_inv_image, wf_lex_prod, 
+				   wf_less_than, wf_trancl] 1),
+    terminator = asm_simp_tac ss 1
+		 THEN TRY(best_tac
+			  (!claset addSDs [not0_implies_Suc] addss ss) 1),
+    simplifier = Rules.simpl_conv ss []};
 
- (*---------------------------------------------------------------------------
-  * Does some standard things with the termination conditions of a definition:
-  * attempts to prove wellfoundedness of the given relation; simplifies the
-  * non-proven termination conditions; and finally attempts to prove the 
-  * simplified termination conditions.
-  *--------------------------------------------------------------------------*)
- val std_postprocessor = Prim.postprocess{WFtac = WFtac,
-                                    terminator = terminator, 
-                                    simplifier = Rules.simpl_conv simpls};
-
- val simplifier = rewrite_rule (simpls @ #simps(rep_ss (!simpset)) @ 
-                                [pred_list_def]);
-
- fun tflcongs thy = Prim.Context.read() @ (#case_congs(Thry.extract_info thy));
+fun tflcongs thy = Prim.Context.read() @ (#case_congs(Thry.extract_info thy));
 
 
 val concl = #2 o Rules.dest_thm;
@@ -111,17 +88,14 @@
 fun define_i thy fid R eqs = 
   let val dummy = require_thy thy "WF_Rel" "recursive function definitions"
       val {functional,pats} = Prim.mk_functional thy eqs
-      val (thm,thry) = Prim.wfrec_definition0 thy fid R functional
-  in (thry,(thm,pats))
+  in (Prim.wfrec_definition0 thy fid R functional, pats)
   end;
 
 (*lcp's version: takes strings; doesn't return "thm" 
         (whose signature is a draft and therefore useless) *)
 fun define thy fid R eqs = 
   let fun read thy = readtm (sign_of thy) (TVar(("DUMMY",0),[])) 
-      val (thy',(_,pats)) =
-             define_i thy fid (read thy R) (map (read thy) eqs)
-  in  (thy',pats)  end
+  in  define_i thy fid (read thy R) (map (read thy) eqs)  end
   handle Utils.ERR {mesg,...} => error mesg;
 
 (*---------------------------------------------------------------------------
@@ -147,8 +121,9 @@
      Const("==",_)$_$_ => r
   |   _$(Const("op =",_)$_$_) => r RS eq_reflection
   |   _ => r RS P_imp_P_eq_True
+
+(*Is this the best way to invoke the simplifier??*)
 fun rewrite L = rewrite_rule (map mk_meta_eq (filter(not o id_thm) L))
-fun reducer thl = rewrite (map standard thl @ #simps(rep_ss (!simpset)))
 
 fun join_assums th = 
   let val {sign,...} = rep_thm th
@@ -164,17 +139,12 @@
   end
   val gen_all = S.gen_all
 in
-(*---------------------------------------------------------------------------
- * The "reducer" argument is 
- *  (fn thl => rewrite (map standard thl @ #simps(rep_ss (!simpset)))); 
- *---------------------------------------------------------------------------*)
-fun proof_stage theory reducer {f, R, rules, full_pats_TCs, TCs} =
+fun proof_stage ss theory {f, R, rules, full_pats_TCs, TCs} =
   let val dummy = prs "Proving induction theorem..  "
       val ind = Prim.mk_induction theory f R full_pats_TCs
-      val dummy = writeln "Proved induction theorem."
-      val pp = std_postprocessor theory
-      val dummy = prs "Postprocessing..  "
-      val {rules,induction,nested_tcs} = pp{rules=rules,induction=ind,TCs=TCs}
+      val dummy = prs "Proved induction theorem.\nPostprocessing..  "
+      val {rules, induction, nested_tcs} = 
+	  std_postprocessor ss theory {rules=rules, induction=ind, TCs=TCs}
   in
   case nested_tcs
   of [] => (writeln "Postprocessing done.";
@@ -186,8 +156,9 @@
                      if (solved th) then (th::So, Si, St) 
                      else (So, th::Si, St)) nested_tcs ([],[],[])
               val simplified' = map join_assums simplified
-              val induction' = reducer (solved@simplified') induction
-              val rules' = reducer (solved@simplified') rules
+              val rewr = rewrite (solved @ simplified' @ #simps(rep_ss ss))
+              val induction' = rewr induction
+              and rules'     = rewr rules
               val dummy = writeln "Postprocessing done."
           in
           {induction = induction',
@@ -212,18 +183,20 @@
 (*Strip off the outer !P*)
 val spec'= read_instantiate [("x","P::?'b=>bool")] spec;
 
+val wf_rel_defs = [lex_prod_def, measure_def, inv_image_def];
 
-fun simplify_defn (thy,(id,pats)) =
+fun simplify_defn ss (thy,(id,pats)) =
    let val dummy = deny (id  mem  map ! (stamps_of_thy thy))
                         ("Recursive definition " ^ id ^ 
                          " would clash with the theory of the same name!")
-       val def = freezeT(get_def thy id  RS  meta_eq_to_obj_eq)
+       val def =  freezeT(get_def thy id)   RS   meta_eq_to_obj_eq
+       val ss' = ss addsimps ((less_Suc_eq RS iffD2) :: wf_rel_defs)
        val {theory,rules,TCs,full_pats_TCs,patterns} = 
-                Prim.post_definition (thy,(def,pats))
+                Prim.post_definition ss' (thy,(def,pats))
        val {lhs=f,rhs} = S.dest_eq(concl def)
        val (_,[R,_]) = S.strip_comb rhs
        val {induction, rules, tcs} = 
-             proof_stage theory reducer
+             proof_stage ss' theory 
                {f = f, R = R, rules = rules,
                 full_pats_TCs = full_pats_TCs,
                 TCs = TCs}
@@ -235,8 +208,7 @@
    end
   handle Utils.ERR {mesg,func,module} => 
                error (mesg ^ 
-		      "\n    (In TFL function " ^ module ^ "." ^ func ^ ")")
-       |  e => print_exn e;
+		      "\n    (In TFL function " ^ module ^ "." ^ func ^ ")");
 end;
 
 (*---------------------------------------------------------------------------
@@ -260,7 +232,6 @@
  in {theory = theory, 
      eq_ind = standard (induction RS (rules RS conjI))}
  end
- handle    e              => print_exn e
 end;
 
 
diff -r 91a91790899a -r 2cccd0e3e9ea TFL/rules.new.sml
--- a/TFL/rules.new.sml	Thu Jun 05 13:26:09 1997 +0200
+++ b/TFL/rules.new.sml	Thu Jun 05 13:27:28 1997 +0200
@@ -282,19 +282,6 @@
   end;
 
 
-local fun string_of(s,_) = s
-in
-fun freeze th =
-  let val fth = freezeT th
-      val {prop,sign,...} = rep_thm fth
-      fun mk_inst (Var(v,T)) = 
-          (cterm_of sign (Var(v,T)),
-           cterm_of sign (Free(string_of v, T)))
-      val insts = map mk_inst (term_vars prop)
-  in  instantiate ([],insts) fth  
-  end
-end;
-
 fun MATCH_MP th1 th2 = 
    if (D.is_forall (D.drop_prop(cconcl th1)))
    then MATCH_MP (th1 RS spec) th2
@@ -326,8 +313,8 @@
 fun CHOOSE(fvar,exth) fact =
    let val lam = #2(dest_comb(D.drop_prop(cconcl exth)))
        val redex = capply lam fvar
-       val {sign,t,...} = rep_cterm redex
-       val residue = cterm_of sign (S.beta_conv t)
+       val {sign, t = t$u,...} = rep_cterm redex
+       val residue = cterm_of sign (betapply(t,u))
     in GEN fvar (DISCH residue fact)  RS (exth RS choose_thm)
    end
 end;
@@ -403,12 +390,10 @@
 fun SUBS thl = 
    rewrite_rule (map (fn th => (th RS eq_reflection) handle _ => th) thl);
 
-val simplify = rewrite_rule;
-
 local fun rew_conv mss = rewrite_cterm (true,false) mss (K(K None))
 in
-fun simpl_conv thl ctm = 
- rew_conv (Thm.mss_of (#simps(rep_ss (!simpset))@thl)) ctm
+fun simpl_conv ss thl ctm = 
+ rew_conv (Thm.mss_of (#simps(rep_ss ss)@thl)) ctm
  RS meta_eq_to_obj_eq
 end;
 
@@ -449,13 +434,6 @@
 
 fun get_lhs tm = #lhs(dest_equal (HOLogic.dest_Trueprop tm));
 
-fun variants FV vlist =
-  rev(#1(U.rev_itlist (fn v => fn (V,W) =>
-                        let val v' = S.variant W v
-                        in (v'::V, v'::W) end) 
-                     vlist ([],FV)));
-
-
 fun dest_all(Const("all",_) $ (a as Abs _)) = S.dest_abs a
   | dest_all _ = raise RULES_ERR{func = "dest_all", mesg = "not a !!"};
 
@@ -501,8 +479,8 @@
             let val eq = Logic.strip_imp_concl body
                 val (f,args) = S.strip_comb (get_lhs eq)
                 val (vstrl,_) = S.strip_abs f
-                val names  = map (#1 o dest_Free)
-                                 (variants (term_frees body) vstrl)
+                val names  = variantlist (map (#1 o dest_Free) vstrl,
+					  add_term_names(body, []))
             in get (rst, n+1, (names,n)::L)
             end handle _ => get (rst, n+1, L);
 
@@ -648,12 +626,13 @@
   in (ants,get_lhs eq)
   end;
 
-val pbeta_reduce = simpl_conv [split RS eq_reflection];
-val restricted = U.can(S.find_term
-                       (U.holds(fn c => (#Name(S.dest_const c)="cut"))))
+fun restricted t = is_some (S.find_term
+			    (fn (Const("cut",_)) =>true | _ => false) 
+			    t)
 
-fun CONTEXT_REWRITE_RULE(func,R){cut_lemma, congs, th} =
- let val tc_list = ref[]: term list ref
+fun CONTEXT_REWRITE_RULE (ss, func, R, cut_lemma, congs) th =
+ let val pbeta_reduce = simpl_conv ss [split RS eq_reflection];
+     val tc_list = ref[]: term list ref
      val dummy = term_ref := []
      val dummy = thm_ref  := []
      val dummy = mss_ref  := []
@@ -761,11 +740,9 @@
                * term "f v1..vn" which is a pattern that any full application
                * of "f" will match.
                *-------------------------------------------------------------*)
-              val func_name = #1(dest_Const func handle _ => dest_Free func)
-              fun is_func tm = (#1(dest_Const tm handle _ => dest_Free tm) 
-				= func_name)
-                               handle _ => false
-              val nested = U.can(S.find_term is_func)
+              val func_name = #1(dest_Const func)
+              fun is_func (Const (name,_)) = (name = func_name)
+		| is_func _                = false
               val rcontext = rev cntxt
               val cncl = HOLogic.dest_Trueprop o #prop o rep_thm
               val antl = case rcontext of [] => [] 
@@ -775,7 +752,7 @@
               val dummy = print_cterms "TC:\n" 
 		              [cterm_of sign (HOLogic.mk_Trueprop TC)]
               val dummy = tc_list := (TC :: !tc_list)
-              val nestedp = nested TC
+              val nestedp = is_some (S.find_term is_func TC)
               val dummy = if nestedp then say"nested\n" else say"not_nested\n"
               val dummy = term_ref := ([func,TC]@(!term_ref))
               val th' = if nestedp then raise RULES_ERR{func = "solver", 
@@ -803,12 +780,8 @@
 
 
 
-fun prove (tm,tac) = 
-  let val {t,sign,...} = rep_cterm tm
-      val ptm = cterm_of sign(HOLogic.mk_Trueprop t)
-  in
-  freeze(prove_goalw_cterm [] ptm (fn _ => [tac]))
-  end;
+fun prove (ptm,tac) = 
+    #1 (freeze_thaw (prove_goalw_cterm [] ptm (fn _ => [tac])));
 
 
 end; (* Rules *)
diff -r 91a91790899a -r 2cccd0e3e9ea TFL/rules.sig
--- a/TFL/rules.sig	Thu Jun 05 13:26:09 1997 +0200
+++ b/TFL/rules.sig	Thu Jun 05 13:27:28 1997 +0200
@@ -46,17 +46,15 @@
   val DISJ_CASESL : thm -> thm list -> thm
 
   val SUBS : thm list -> thm -> thm
-  val simplify : thm list -> thm -> thm
-  val simpl_conv : thm list -> cterm -> thm
+  val simpl_conv : simpset -> thm list -> cterm -> thm
 
 (* For debugging my isabelle solver in the conditional rewriter *)
   val term_ref : term list ref
   val thm_ref : thm list ref
   val mss_ref : meta_simpset list ref
   val tracing :bool ref
-  val CONTEXT_REWRITE_RULE : term * term
-                             -> {cut_lemma:thm, congs: thm list, th:thm} 
-                             -> thm * term list
+  val CONTEXT_REWRITE_RULE : simpset * term * term * thm * thm list 
+                             -> thm -> thm * term list
   val RIGHT_ASSOC : thm -> thm 
 
   val prove : cterm * tactic -> thm
diff -r 91a91790899a -r 2cccd0e3e9ea TFL/tfl.sig
--- a/TFL/tfl.sig	Thu Jun 05 13:26:09 1997 +0200
+++ b/TFL/tfl.sig	Thu Jun 05 13:27:28 1997 +0200
@@ -15,23 +15,22 @@
                        -> {functional:term,
                            pats: pattern list}
 
-   val wfrec_definition0 : theory -> string -> term -> term -> thm * theory
+   val wfrec_definition0 : theory -> string -> term -> term -> theory
 
-   val post_definition : theory * (thm * pattern list)
-                              -> {theory : theory,
-                                  rules  : thm, 
-                                    TCs  : term list list,
-                          full_pats_TCs  : (term * term list) list, 
-                               patterns  : pattern list}
+   val post_definition : simpset -> theory * (thm * pattern list)
+				 -> {theory : theory,
+				     rules  : thm, 
+				       TCs  : term list list,
+			     full_pats_TCs  : (term * term list) list, 
+				  patterns  : pattern list}
 
-
+(*CURRENTLY UNUSED
    val wfrec_eqns : theory -> term list
                      -> {WFR : term, 
                          proto_def : term,
                          extracta :(thm * term list) list,
                          pats  : pattern list}
 
-
    val lazyR_def : theory
                    -> term list
                    -> {theory:theory,
@@ -39,11 +38,9 @@
                            R :term,
                        full_pats_TCs :(term * term list) list, 
                        patterns: pattern list}
+---------------------*)
 
-   val mk_induction : theory 
-                       -> term -> term 
-                         -> (term * term list) list
-                           -> thm
+   val mk_induction : theory -> term -> term -> (term * term list) list -> thm
 
    val postprocess: {WFtac:tactic, terminator:tactic, simplifier:cterm -> thm}
                      -> theory 
diff -r 91a91790899a -r 2cccd0e3e9ea TFL/tfl.sml
--- a/TFL/tfl.sml	Thu Jun 05 13:26:09 1997 +0200
+++ b/TFL/tfl.sml	Thu Jun 05 13:27:28 1997 +0200
@@ -43,12 +43,12 @@
  * proof of completeness of cases for the induction theorem.
  *
  * The curried function "gvvariant" returns a function to generate distinct
- * variables that are guaranteed not to be in vlist.  The names of
+ * variables that are guaranteed not to be in names.  The names of
  * the variables go u, v, ..., z, aa, ..., az, ...  The returned 
  * function contains embedded refs!
  *---------------------------------------------------------------------------*)
-fun gvvariant vlist =
-  let val slist = ref (map (#1 o dest_Free) vlist)
+fun gvvariant names =
+  let val slist = ref names
       val vname = ref "u"
       fun new() = 
          if !vname mem_string (!slist)
@@ -189,10 +189,10 @@
  * incomplete set of patterns is given.
  *---------------------------------------------------------------------------*)
 
-fun mk_case ty_info ty_match FV range_ty =
+fun mk_case ty_info ty_match usednames range_ty =
  let 
  fun mk_case_fail s = raise TFL_ERR{func = "mk_case", mesg = s}
- val fresh_var = gvvariant FV 
+ val fresh_var = gvvariant usednames 
  val divide = partition fresh_var ty_match
  fun expand constructors ty ((_,[]), _) = mk_case_fail"expand_var_row"
    | expand constructors ty (row as ((prefix, p::rst), rhs)) = 
@@ -285,19 +285,18 @@
  let val (L,R) = ListPair.unzip 
                     (map (fn (Const("op =",_) $ t $ u) => (t,u)) clauses)
      val (funcs,pats) = ListPair.unzip (map (fn (t$u) =>(t,u)) L)
-     val f = single (gen_distinct (op aconv) funcs)
-     (**??why change the Const to a Free??????????????**)
-     val fvar = if (is_Free f) then f else Free(dest_Const f)
+     val fcon as Const (fname, ftype) = single (gen_distinct (op aconv) funcs)
      val dummy = map (no_repeat_vars thy) pats
      val rows = ListPair.zip (map (fn x => ([],[x])) pats,
                               map GIVEN (enumerate R))
-     val fvs = S.free_varsl R
-     val a = S.variant fvs (Free("a",type_of(hd pats)))
-     val FV = a::fvs
+     val names = foldr add_term_names (R,[])
+     val atype = type_of(hd pats)
+     and aname = variant names "a"
+     val a = Free(aname,atype)
      val ty_info = Thry.match_info thy
      val ty_match = Thry.match_type thy
      val range_ty = type_of (hd R)
-     val (patts, case_tm) = mk_case ty_info ty_match FV range_ty 
+     val (patts, case_tm) = mk_case ty_info ty_match (aname::names) range_ty 
                                     {path=[a], rows=rows}
      val patts1 = map (fn (_,(tag,i),[pat]) => tag (pat,i)) patts 
 	  handle _ => mk_functional_err "error in pattern-match translation"
@@ -308,8 +307,9 @@
              of [] => ()
           | L => mk_functional_err("The following rows (counting from zero)\
                                    \ are inaccessible: "^stringize L)
-     val case_tm' = subst_free [(f,fvar)] case_tm
- in {functional = S.list_mk_abs ([fvar,a], case_tm'),
+ in {functional = Abs(fname, ftype, 
+		      abstract_over (fcon, 
+				     absfree(aname,atype, case_tm))),
      pats = patts2}
 end end;
 
@@ -326,10 +326,6 @@
   | poly_tvars (TFree (a,sort)) = TVar (("?" ^ a, 0), sort)
   | poly_tvars (TVar ((a,i),sort)) = TVar (("?" ^ a, i+1), sort);
 
-
-(*---------------------------------------------------------------------------
- * R is already assumed to be type-copacetic with M
- *---------------------------------------------------------------------------*)
 local val f_eq_wfrec_R_M = 
            #ant(S.dest_imp(#2(S.strip_forall (concl Thms.WFREC_COROLLARY))))
       val {lhs=f, rhs} = S.dest_eq f_eq_wfrec_R_M
@@ -348,12 +344,9 @@
 	              $ functional
      val (_, def_term, _) = 
 	 Sign.infer_types (sign_of thy) (K None) (K None) [] false
-	       ([HOLogic.mk_eq(Const(Name,Ty), wfrec_R_M)], 
-		HOLogic.boolT)
-		    
-  in 
-  Thry.make_definition thy def_name def_term
-  end
+	       ([Const("==",dummyT) $ Const(Name,Ty) $ wfrec_R_M], 
+		propT)
+  in  add_defs_i [(def_name, def_term)] thy  end
 end;
 
 
@@ -396,15 +389,11 @@
 end;
 
 
-(*Replace all TFrees by TVars [CURRENTLY UNUSED]*)
-val tvars_of_tfrees = 
-    map_term_types (map_type_tfree (fn (a,sort) => TVar ((a, 0), sort)));
-
 fun givens [] = []
   | givens (GIVEN(tm,_)::pats) = tm :: givens pats
   | givens (OMITTED _::pats)   = givens pats;
 
-fun post_definition (theory, (def, pats)) =
+fun post_definition ss (theory, (def, pats)) =
  let val tych = Thry.typecheck theory 
      val f = #lhs(S.dest_eq(concl def))
      val corollary = R.MATCH_MP Thms.WFREC_COROLLARY def
@@ -415,14 +404,14 @@
      val corollaries = map (fn pat => R.SPEC (tych pat) corollary') 
 	                   given_pats
      val (case_rewrites,context_congs) = extraction_thms theory
-     val corollaries' = map(R.simplify case_rewrites) corollaries
-     fun xtract th = R.CONTEXT_REWRITE_RULE(f,R)
-                         {cut_lemma = R.ISPECL (map tych [f,R]) Thms.CUT_LEMMA,
-			  congs = context_congs,
-			  th = th}
-     val (rules, TCs) = ListPair.unzip (map xtract corollaries')
-     val rules0 = map (R.simplify [Thms.CUT_DEF]) rules
-     val mk_cond_rule = R.FILTER_DISCH_ALL(not o S.aconv WFR)
+     val corollaries' = map(rewrite_rule case_rewrites) corollaries
+     val extract = R.CONTEXT_REWRITE_RULE 
+	             (ss, f, R,
+		      R.ISPECL (map tych [f,R]) Thms.CUT_LEMMA,
+		      context_congs)
+     val (rules, TCs) = ListPair.unzip (map extract corollaries')
+     val rules0 = map (rewrite_rule [Thms.CUT_DEF]) rules
+     val mk_cond_rule = R.FILTER_DISCH_ALL(not o curry (op aconv) WFR)
      val rules1 = R.LIST_CONJ(map mk_cond_rule rules0)
  in
  {theory = theory,   (* holds def, if it's needed *)
@@ -437,8 +426,8 @@
  * Perform the extraction without making the definition. Definition and
  * extraction commute for the non-nested case. For hol90 users, this 
  * function can be invoked without being in draft mode.
- *---------------------------------------------------------------------------*)
-fun wfrec_eqns thy eqns =
+ * CURRENTLY UNUSED
+fun wfrec_eqns ss thy eqns =
  let val {functional,pats} = mk_functional thy eqns
      val given_pats = givens pats
      val {Bvar = f, Body} = S.dest_abs functional
@@ -447,23 +436,25 @@
      val (case_rewrites,context_congs) = extraction_thms thy
      val tych = Thry.typecheck thy
      val WFREC_THM0 = R.ISPEC (tych functional) Thms.WFREC_COROLLARY
-     val R = S.variant(foldr add_term_frees (eqns,[])) 
-                      (#Bvar(S.dest_forall(concl WFREC_THM0)))
+     val Const("All",_) $ Abs(Rname,Rtype,_) = concl WFREC_THM0
+     val R = Free (variant (foldr add_term_names (eqns,[])) Rname,
+		   Rtype)
      val WFREC_THM = R.ISPECL [tych R, tych f] WFREC_THM0
      val ([proto_def, WFR],_) = S.strip_imp(concl WFREC_THM)
      val R1 = S.rand WFR
      val corollary' = R.UNDISCH(R.UNDISCH WFREC_THM)
-     val corollaries = map (U.C R.SPEC corollary' o tych) given_pats
-     val corollaries' = map (R.simplify case_rewrites) corollaries
-     fun extract th = R.CONTEXT_REWRITE_RULE(f,R1)
-                        {cut_lemma = R.ISPECL (map tych [f,R1]) Thms.CUT_LEMMA,
-			 congs = context_congs,
-			 th  = th}
+     val corollaries = map (fn pat => R.SPEC (tych pat) corollary') given_pats
+     val corollaries' = map (rewrite_rule case_rewrites) corollaries
+     val extract = R.CONTEXT_REWRITE_RULE 
+	               (ss, f, R1, 
+		        R.ISPECL (map tych [f,R1]) Thms.CUT_LEMMA, 
+			context_congs)
  in {proto_def=proto_def, 
      WFR=WFR, 
      pats=pats,
      extracta = map extract corollaries'}
  end;
+ *---------------------------------------------------------------------------*)
 
 
 (*---------------------------------------------------------------------------
@@ -471,9 +462,9 @@
  * wellfounded relation used in the definition is computed by using the
  * choice operator on the extracted conditions (plus the condition that
  * such a relation must be wellfounded).
- *---------------------------------------------------------------------------*)
-fun lazyR_def thy eqns =
- let val {proto_def,WFR,pats,extracta} = wfrec_eqns thy eqns
+ * CURRENTLY UNUSED
+fun lazyR_def ss thy eqns =
+ let val {proto_def,WFR,pats,extracta} = wfrec_eqns ss thy eqns
      val R1 = S.rand WFR
      val f = S.lhs proto_def
      val (Name,_) = dest_Free f
@@ -482,8 +473,9 @@
      val full_rqt = WFR::TCs
      val R' = S.mk_select{Bvar=R1, Body=S.list_mk_conj full_rqt}
      val R'abs = S.rand R'
-     val (def,theory) = Thry.make_definition thy (Name ^ "_def") 
-                                               (subst_free[(R1,R')] proto_def)
+     val theory = add_defs_i [(Name ^ "_def", subst_free[(R1,R')] proto_def)]
+	                     thy
+     val def = freezeT((get_axiom theory (Name ^ "_def")) RS meta_eq_to_obj_eq)
      val fconst = #lhs(S.dest_eq(concl def)) 
      val tych = Thry.typecheck theory
      val baz = R.DISCH (tych proto_def)
@@ -499,6 +491,7 @@
      full_pats_TCs = merge (map pat_of pats) (ListPair.zip (givens pats, TCl)),
      patterns = pats}
  end;
+ *---------------------------------------------------------------------------*)
 
 
 
@@ -535,10 +528,10 @@
       val args = map (fn qv => the (gen_assoc (op aconv) (plist, qv))) qvars
                    handle OPTION _ => error 
                        "TFL fault [alpha_ex_unroll]: no correspondence"
-      fun build ex [] = []
-        | build ex (v::rst) =
-           let val ex1 = S.beta_conv(S.mk_comb{Rator=S.rand ex, Rand=v})
-           in ex1::build ex1 rst
+      fun build ex      []   = []
+        | build (_$rex) (v::rst) =
+           let val ex1 = betapply(rex, v)
+           in  ex1 :: build ex1 rst
            end
      val (nex::exl) = rev (tm::build tm args)
   in 
@@ -553,9 +546,9 @@
  *
  *---------------------------------------------------------------------------*)
 
-fun mk_case ty_info FV thy =
+fun mk_case ty_info usednames thy =
  let 
- val divide = ipartition (gvvariant FV)
+ val divide = ipartition (gvvariant usednames)
  val tych = Thry.typecheck thy
  fun tych_binding(x,y) = (tych x, tych y)
  fun fail s = raise TFL_ERR{func = "mk_case", mesg = s}
@@ -608,11 +601,12 @@
  let val tych = Thry.typecheck thy
      val ty_info = Thry.induct_info thy
  in fn pats =>
- let val FV0 = S.free_varsl pats
+ let val names = foldr add_term_names (pats,[])
      val T = type_of (hd pats)
-     val a = S.variant FV0 (Free ("a", T))
-     val v = S.variant (a::FV0) (Free ("v", T))
-     val FV = a::v::FV0
+     val aname = Term.variant names "a"
+     val vname = Term.variant (aname::names) "v"
+     val a = Free (aname, T)
+     val v = Free (vname, T)
      val a_eq_v = HOLogic.mk_eq(a,v)
      val ex_th0 = R.EXISTS (tych (S.mk_exists{Bvar=v,Body=a_eq_v}), tych a)
                            (R.REFL (tych a))
@@ -622,7 +616,8 @@
  R.GEN (tych a) 
        (R.RIGHT_ASSOC
           (R.CHOOSE(tych v, ex_th0)
-                (mk_case ty_info FV thy {path=[v], rows=rows})))
+                (mk_case ty_info (vname::aname::names)
+		 thy {path=[v], rows=rows})))
  end end;
 
 
@@ -636,29 +631,28 @@
  * Note. When the context is empty, there can be no local variables.
  *---------------------------------------------------------------------------*)
 
-local nonfix ^ ;   infix 9 ^  ;     infix 5 ==>
-      fun (tm1 ^ tm2)   = S.mk_comb{Rator = tm1, Rand = tm2}
+local infix 5 ==>
       fun (tm1 ==> tm2) = S.mk_imp{ant = tm1, conseq = tm2}
 in
 fun build_ih f P (pat,TCs) = 
  let val globals = S.free_vars_lr pat
-     fun nested tm = U.can(S.find_term (S.aconv f)) tm handle _ => false
+     fun nested tm = is_some (S.find_term (curry (op aconv) f) tm)
      fun dest_TC tm = 
          let val (cntxt,R_y_pat) = S.strip_imp(#2(S.strip_forall tm))
              val (R,y,_) = S.dest_relation R_y_pat
-             val P_y = if (nested tm) then R_y_pat ==> P^y else P^y
+             val P_y = if (nested tm) then R_y_pat ==> P$y else P$y
          in case cntxt 
               of [] => (P_y, (tm,[]))
                | _  => let 
                     val imp = S.list_mk_conj cntxt ==> P_y
                     val lvs = gen_rems (op aconv) (S.free_vars_lr imp, globals)
-                    val locals = #2(U.pluck (S.aconv P) lvs) handle _ => lvs
+                    val locals = #2(U.pluck (curry (op aconv) P) lvs) handle _ => lvs
                     in (S.list_mk_forall(locals,imp), (tm,locals)) end
          end
  in case TCs
-    of [] => (S.list_mk_forall(globals, P^pat), [])
+    of [] => (S.list_mk_forall(globals, P$pat), [])
      |  _ => let val (ihs, TCs_locals) = ListPair.unzip(map dest_TC TCs)
-                 val ind_clause = S.list_mk_conj ihs ==> P^pat
+                 val ind_clause = S.list_mk_conj ihs ==> P$pat
              in (S.list_mk_forall(globals,ind_clause), TCs_locals)
              end
  end
@@ -678,7 +672,7 @@
  let val tych = Thry.typecheck thy
      val antc = tych(#ant(S.dest_imp tm))
      val thm' = R.SPEC_ALL thm
-     fun nested tm = U.can(S.find_term (S.aconv f)) tm handle _ => false
+     fun nested tm = is_some (S.find_term (curry (op aconv) f) tm)
      fun get_cntxt TC = tych(#ant(S.dest_imp(#2(S.strip_forall(concl TC)))))
      fun mk_ih ((TC,locals),th2,nested) =
          R.GENL (map tych locals)
@@ -723,9 +717,6 @@
   in  #2 (U.itlist CHOOSER L (veq,thm))  end;
 
 
-fun combize M N = S.mk_comb{Rator=M,Rand=N};
-
-
 (*----------------------------------------------------------------------------
  * Input : f, R,  and  [(pat1,TCs1),..., (patn,TCsn)]
  *
@@ -739,18 +730,20 @@
     val (pats,TCsl) = ListPair.unzip pat_TCs_list
     val case_thm = complete_cases thy pats
     val domain = (type_of o hd) pats
-    val P = S.variant (S.all_varsl (pats @ List_.concat TCsl))
-                      (Free("P",domain --> HOLogic.boolT))
+    val Pname = Term.variant (foldr (foldr add_term_names) 
+			      (pats::TCsl, [])) "P"
+    val P = Free(Pname, domain --> HOLogic.boolT)
     val Sinduct = R.SPEC (tych P) Sinduction
     val Sinduct_assumf = S.rand ((#ant o S.dest_imp o concl) Sinduct)
     val Rassums_TCl' = map (build_ih f P) pat_TCs_list
     val (Rassums,TCl') = ListPair.unzip Rassums_TCl'
     val Rinduct_assum = R.ASSUME (tych (S.list_mk_conj Rassums))
-    val cases = map (S.beta_conv o combize Sinduct_assumf) pats
+    val cases = map (fn pat => betapply (Sinduct_assumf, pat)) pats
     val tasks = U.zip3 cases TCl' (R.CONJUNCTS Rinduct_assum)
     val proved_cases = map (prove_case f thy) tasks
-    val v = S.variant (S.free_varsl (map concl proved_cases))
-                      (Free("v",domain))
+    val v = Free (variant (foldr add_term_names (map concl proved_cases, []))
+		    "v",
+		  domain)
     val vtyped = tych v
     val substs = map (R.SYM o R.ASSUME o tych o (curry HOLogic.mk_eq v)) pats
     val proved_cases1 = ListPair.map (fn (th,th') => R.SUBS[th]th') 
@@ -759,7 +752,7 @@
     val dant = R.GEN vtyped (R.DISJ_CASESL (R.ISPEC vtyped case_thm) abs_cases)
     val dc = R.MP Sinduct dant
     val Parg_ty = type_of(#Bvar(S.dest_forall(concl dc)))
-    val vars = map (gvvariant[P]) (S.strip_prod_type Parg_ty)
+    val vars = map (gvvariant[Pname]) (S.strip_prod_type Parg_ty)
     val dc' = U.itlist (R.GEN o tych) vars
                        (R.SPEC (tych(S.mk_vstruct Parg_ty vars)) dc)
 in 
@@ -809,7 +802,9 @@
     * Attempt to eliminate WF condition. It's the only assumption of rules
     *---------------------------------------------------------------------*)
    val (rules1,induction1)  = 
-       let val thm = R.prove(tych(hd(#1(R.dest_thm rules))),WFtac)
+       let val thm = R.prove(tych(HOLogic.mk_Trueprop 
+				  (hd(#1(R.dest_thm rules)))),
+			     WFtac)
        in (R.PROVE_HYP thm rules,  R.PROVE_HYP thm induction)
        end handle _ => (rules,induction)
 
@@ -827,7 +822,8 @@
        elim_tc (R.MATCH_MP Thms.eqT tc_eq) (r,ind)
        handle _ => 
         (elim_tc (R.MATCH_MP(R.MATCH_MP Thms.rev_eq_mp tc_eq)
-                            (R.prove(tych(S.rhs(concl tc_eq)),terminator)))
+		  (R.prove(tych(HOLogic.mk_Trueprop(S.rhs(concl tc_eq))), 
+			   terminator)))
                  (r,ind)
          handle _ => 
           (R.UNDISCH(R.MATCH_MP (R.MATCH_MP Thms.simp_thm r) tc_eq), 
@@ -854,7 +850,8 @@
        (R.MATCH_MP Thms.eqT tc_eq
         handle _
         => (R.MATCH_MP(R.MATCH_MP Thms.rev_eq_mp tc_eq)
-                      (R.prove(tych(S.rhs(concl tc_eq)),terminator))
+                      (R.prove(tych(HOLogic.mk_Trueprop (S.rhs(concl tc_eq))),
+			       terminator))
             handle _ => tc_eq))
       end
 
diff -r 91a91790899a -r 2cccd0e3e9ea TFL/thry.sig
--- a/TFL/thry.sig	Thu Jun 05 13:26:09 1997 +0200
+++ b/TFL/thry.sig	Thu Jun 05 13:27:28 1997 +0200
@@ -6,7 +6,6 @@
 
 signature Thry_sig =
 sig
-  structure USyntax : USyntax_sig
   val match_term : theory -> term -> term 
                     -> (term*term)list * (typ*typ)list
 
@@ -14,8 +13,6 @@
 
   val typecheck : theory -> term -> cterm
 
-  val make_definition: theory -> string -> term -> thm * theory
-
   (* Datatype facts of various flavours *)
   val match_info: theory -> string -> {constructors:term list,
                                      case_const:term} option
diff -r 91a91790899a -r 2cccd0e3e9ea TFL/thry.sml
--- a/TFL/thry.sml	Thu Jun 05 13:26:09 1997 +0200
+++ b/TFL/thry.sml	Thu Jun 05 13:27:28 1997 +0200
@@ -7,7 +7,6 @@
 structure Thry : Thry_sig (* LThry_sig *) = 
 struct
 
-structure USyntax  = USyntax;
 structure S = USyntax;
 
 fun THRY_ERR{func,mesg} = Utils.ERR{module = "Thry",func=func,mesg=mesg};
@@ -37,55 +36,6 @@
 fun typecheck thry = cterm_of (sign_of thry);
 
 
-
-(*----------------------------------------------------------------------------
- * Making a definition. The argument "tm" looks like "f = WFREC R M". This 
- * entrypoint is specialized for interactive use, since it closes the theory
- * after making the definition. This allows later interactive definitions to
- * refer to previous ones. The name for the new theory is automatically 
- * generated from the name of the argument theory.
- *---------------------------------------------------------------------------*)
-
-
-(*---------------------------------------------------------------------------
- * TFL attempts to make definitions where the lhs is a variable. Isabelle
- * wants it to be a constant, so here we map it to a constant. Moreover, the
- * theory should already have the constant, so we refrain from adding the
- * constant to the theory. We just add the axiom and return the theory.
- *---------------------------------------------------------------------------*)
-local val (imp $ tprop $ (eeq $ _ $ _ )) = #prop(rep_thm(eq_reflection))
-      val Const(eeq_name, ty) = eeq
-      val prop = body_type ty
-in
-fun make_definition parent s tm = 
-   let val {lhs,rhs} = S.dest_eq tm
-       val (_,Ty) = dest_Const lhs
-       val eeq1 = Const(eeq_name, Ty --> Ty --> prop)
-       val dtm = list_comb(eeq1,[lhs,rhs])      (* Rename "=" to "==" *)
-       val (_, tm', _) = Sign.infer_types (sign_of parent)
-                     (K None) (K None) [] true ([dtm],propT)
-       val new_thy = add_defs_i [(s,tm')] parent
-   in 
-   (freezeT((get_axiom new_thy s) RS meta_eq_to_obj_eq), new_thy)
-   end;
-end;
-
-(*---------------------------------------------------------------------------
- * Utility routine. Insert into list ordered by the key (a string). If two 
- * keys are equal, the new element replaces the old. A more efficient option 
- * for the future is needed. In fact, having the list of datatype facts be 
- * ordered is useless, since the lookup should never fail!
- *---------------------------------------------------------------------------*)
-fun insert (el as (x:string, _)) = 
- let fun canfind[] = [el] 
-       | canfind(alist as ((y as (k,_))::rst)) = 
-           if (x<k) then el::alist
-           else if (x=k) then el::rst
-           else y::canfind rst 
- in canfind
- end;
-
-
 (*---------------------------------------------------------------------------
  *     A collection of facts about datatypes
  *---------------------------------------------------------------------------*)
diff -r 91a91790899a -r 2cccd0e3e9ea TFL/usyntax.sig
--- a/TFL/usyntax.sig	Thu Jun 05 13:26:09 1997 +0200
+++ b/TFL/usyntax.sig	Thu Jun 05 13:27:28 1997 +0200
@@ -25,21 +25,14 @@
   val strip_prod_type : typ -> typ list
 
   (* Terms *)
-  val free_varsl : term list -> term list
   val free_vars_lr : term -> term list
-  val all_vars   : term -> term list
-  val all_varsl  : term list -> term list
-  val variant    : term list -> term -> term
   val type_vars_in_term : term -> typ list
   val dest_term  : term -> lambda
   
   (* Prelogic *)
-  val aconv     : term -> term -> bool
   val inst      : (typ*typ) list -> term -> term
-  val beta_conv : term -> term
 
   (* Construction routines *)
-  val mk_comb   :{Rator : term, Rand : term} -> term
   val mk_abs    :{Bvar  : term, Body : term} -> term
 
   val mk_imp    :{ant : term, conseq :  term} -> term
@@ -66,14 +59,9 @@
 
   val lhs   : term -> term
   val rhs   : term -> term
-  val rator : term -> term
   val rand  : term -> term
-  val bvar  : term -> term
-  val body  : term -> term
-  
 
   (* Query routines *)
-  val is_eq     : term -> bool
   val is_imp    : term -> bool
   val is_forall : term -> bool 
   val is_exists : term -> bool 
@@ -87,7 +75,6 @@
   val list_mk_abs    : (term list * term) -> term
   val list_mk_imp    : (term list * term) -> term
   val list_mk_forall : (term list * term) -> term
-  val list_mk_exists : (term list * term) -> term
   val list_mk_conj   : term list -> term
   val list_mk_disj   : term list -> term
 
@@ -102,8 +89,7 @@
   (* Miscellaneous *)
   val mk_vstruct : typ -> term list -> term
   val gen_all    : term -> term
-  val find_term  : (term -> bool) -> term -> term
-  val find_terms : (term -> bool) -> term -> term list
+  val find_term  : (term -> bool) -> term -> term option
   val dest_relation : term -> term * term * term
   val is_WFR : term -> bool
   val ARB : typ -> term
diff -r 91a91790899a -r 2cccd0e3e9ea TFL/usyntax.sml
--- a/TFL/usyntax.sml	Thu Jun 05 13:26:09 1997 +0200
+++ b/TFL/usyntax.sml	Thu Jun 05 13:27:28 1997 +0200
@@ -49,9 +49,6 @@
  *                              Terms 
  *
  *---------------------------------------------------------------------------*)
-nonfix aconv;
-val aconv = curry (op aconv);
-
 
 (* Free variables, in order of occurrence, from left to right in the 
  * syntax tree. *)
@@ -67,52 +64,17 @@
 
 
 
-fun free_varsl L = gen_distinct Term.aconv
-                      (Utils.rev_itlist (curry op @ o term_frees) L []);
-
 val type_vars_in_term = map mk_prim_vartype o term_tvars;
 
-fun all_vars tm = 
-  let fun memb x = let fun m[] = false | m(y::rst) = (x=y)orelse m rst in m end
-      fun add (t, A) = case t of
-            Free   _ => if (memb t A) then A else t::A
-          | Abs (s,ty,body) => add(body, add(Free(s,ty),A))
-          | f$t =>  add(t, add(f, A))
-          | _ => A
-  in rev(add(tm,[]))
-  end;
-fun all_varsl L = gen_distinct Term.aconv
-                      (Utils.rev_itlist (curry op @ o all_vars) L []);
 
 
 (* Prelogic *)
 fun dest_tybinding (v,ty) = (#1(dest_vtype v),ty)
 fun inst theta = subst_vars (map dest_tybinding theta,[])
 
-fun beta_conv((t1 as Abs _ ) $ t2) = betapply(t1,t2)
-  | beta_conv _ = raise USYN_ERR{func = "beta_conv", mesg = "Not a beta-redex"};
-
 
 (* Construction routines *)
 
-val string_variant = variant;
-
-local fun var_name(Var((Name,_),_)) = Name
-        | var_name(Free(s,_)) = s
-        | var_name _ = raise USYN_ERR{func = "variant",
-                                 mesg = "list elem. is not a variable"}
-in
-fun variant [] v = v
-  | variant vlist (Var((Name,i),ty)) = 
-       Var((string_variant (map var_name vlist) Name,i),ty)
-  | variant vlist (Free(Name,ty)) =
-       Free(string_variant (map var_name vlist) Name,ty)
-  | variant _ _ = raise USYN_ERR{func = "variant",
-                            mesg = "2nd arg. should be a variable"}
-end;
-
-fun mk_comb{Rator,Rand} = Rator $ Rand;
-
 fun mk_abs{Bvar as Var((s,_),ty),Body}  = Abs(s,ty,abstract_over(Bvar,Body))
   | mk_abs{Bvar as Free(s,ty),Body}  = Abs(s,ty,abstract_over(Bvar,Body))
   | mk_abs _ = raise USYN_ERR{func = "mk_abs", mesg = "Bvar is not a variable"};
@@ -166,8 +128,8 @@
        if (is_var varstruct)
        then mk_abs{Bvar = varstruct, Body = body}
        else let val {fst,snd} = dest_pair varstruct
-            in mk_comb{Rator= mk_uncurry(type_of fst,type_of snd,type_of body),
-                       Rand = mpa(fst,mpa(snd,body))}
+            in mk_uncurry(type_of fst,type_of snd,type_of body) $
+	       mpa(fst,mpa(snd,body))
             end
  in mpa(varstruct,body)
  end
@@ -255,16 +217,10 @@
 (* Garbage - ought to be dropped *)
 val lhs   = #lhs o dest_eq
 val rhs   = #rhs o dest_eq
-val rator = #Rator o dest_comb
 val rand  = #Rand o dest_comb
-val bvar  = #Bvar o dest_abs
-val body  = #Body o dest_abs
   
 
 (* Query routines *)
-val is_comb   = can dest_comb
-val is_abs    = can dest_abs
-val is_eq     = can dest_eq
 val is_imp    = can dest_imp
 val is_forall = can dest_forall
 val is_exists = can dest_exists
@@ -281,7 +237,6 @@
 
 (* These others are almost never used *)
 fun list_mk_imp(A,c) = itlist(fn a => fn tm => mk_imp{ant=a,conseq=tm}) A c;
-fun list_mk_exists(V,t) = itlist(fn v => fn b => mk_exists{Bvar=v, Body=b})V t;
 fun list_mk_forall(V,t) = itlist(fn v => fn b => mk_forall{Bvar=v, Body=b})V t;
 val list_mk_conj = end_itlist(fn c1 => fn tm => mk_conj{conj1=c1, conj2=tm})
 val list_mk_disj = end_itlist(fn d1 => fn tm => mk_disj{disj1=d1, disj2=tm})
@@ -352,35 +307,14 @@
 (* Search a term for a sub-term satisfying the predicate p. *)
 fun find_term p =
    let fun find tm =
-      if (p tm)
-      then tm 
-      else if (is_abs tm)
-           then find (#Body(dest_abs tm))
-           else let val {Rator,Rand} = dest_comb tm
-                in find Rator handle _ => find Rand
-                end handle _ => raise USYN_ERR{func = "find_term",mesg = ""}
+      if (p tm) then Some tm 
+      else case tm of
+	  Abs(_,_,body) => find body
+	| (t$u)         => (Some (the (find t)) handle _ => find u)
+	| _             => None
    in find
    end;
 
-(*******************************************************************
- * find_terms: (term -> HOLogic.boolT) -> term -> term list
- * 
- *  Find all subterms in a term that satisfy a given predicate p.
- *
- *******************************************************************)
-fun find_terms p =
-   let fun accum tl tm =
-      let val tl' = if (p tm) then (tm::tl) else tl 
-      in if (is_abs tm)
-         then accum tl' (#Body(dest_abs tm))
-         else let val {Rator,Rand} = dest_comb tm
-              in accum (accum tl' Rator) Rand
-              end handle _ => tl'
-      end
-   in accum []
-   end;
-
-
 fun dest_relation tm =
    if (type_of tm = HOLogic.boolT)
    then let val (Const("op :",_) $ (Const("Pair",_)$y$x) $ R) = tm
@@ -389,7 +323,8 @@
                                   mesg="unexpected term structure"}
    else raise USYN_ERR{func="dest_relation",mesg="not a boolean term"};
 
-fun is_WFR tm = (#Name(dest_const(rator tm)) = "wf") handle _ => false;
+fun is_WFR (Const("wf",_)$_) = true
+  | is_WFR _                 = false;
 
 fun ARB ty = mk_select{Bvar=Free("v",ty),
                        Body=Const("True",HOLogic.boolT)};