tuned;

--- a/TFL/post.ML	Wed Nov 09 16:26:53 2005 +0100
+++ b/TFL/post.ML	Wed Nov 09 16:26:54 2005 +0100
@@ -43,7 +43,7 @@
  *--------------------------------------------------------------------------*)
 fun termination_goals rules =
     map (Type.freeze o HOLogic.dest_Trueprop)
-      (foldr (fn (th,A) => union_term (prems_of th, A)) [] rules);
+      (foldr (fn (th,A) => gen_union (op aconv) (prems_of th, A)) [] rules);
 
 (*---------------------------------------------------------------------------
  * Finds the termination conditions in (highly massaged) definition and

--- a/src/Pure/Syntax/printer.ML	Wed Nov 09 16:26:53 2005 +0100
+++ b/src/Pure/Syntax/printer.ML	Wed Nov 09 16:26:54 2005 +0100
@@ -111,7 +111,7 @@
 (** term_to_ast **)
 
 fun mark_freevars ((t as Const (c, _)) $ u) =
-      if c mem_string SynExt.standard_token_markers then (t $ u)
+      if member (op =) SynExt.standard_token_markers c then (t $ u)
       else t $ mark_freevars u
   | mark_freevars (t $ u) = mark_freevars t $ mark_freevars u
   | mark_freevars (Abs (x, T, t)) = Abs (x, T, mark_freevars t)
@@ -126,11 +126,11 @@
     fun prune_typs (t_seen as (Const _, _)) = t_seen
       | prune_typs (t as Free (x, ty), seen) =
           if ty = dummyT then (t, seen)
-          else if no_freeTs orelse t mem seen then (Lexicon.free x, seen)
+          else if no_freeTs orelse member (op aconv) seen t then (Lexicon.free x, seen)
           else (t, t :: seen)
       | prune_typs (t as Var (xi, ty), seen) =
           if ty = dummyT then (t, seen)
-          else if no_freeTs orelse t mem seen then (Lexicon.var xi, seen)
+          else if no_freeTs orelse member (op aconv) seen t then (Lexicon.var xi, seen)
           else (t, t :: seen)
       | prune_typs (t_seen as (Bound _, _)) = t_seen
       | prune_typs (Abs (x, ty, t), seen) =

--- a/src/Pure/Syntax/syn_trans.ML	Wed Nov 09 16:26:53 2005 +0100
+++ b/src/Pure/Syntax/syn_trans.ML	Wed Nov 09 16:26:54 2005 +0100
@@ -395,10 +395,10 @@
 fun antiquote_tr' name =
   let
     fun tr' i (t $ u) =
-      if u = Bound i then Lexicon.const name $ tr' i t
+      if u aconv Bound i then Lexicon.const name $ tr' i t
       else tr' i t $ tr' i u
       | tr' i (Abs (x, T, t)) = Abs (x, T, tr' (i + 1) t)
-      | tr' i a = if a = Bound i then raise Match else a;
+      | tr' i a = if a aconv Bound i then raise Match else a;
   in tr' 0 end;
 
 fun quote_tr' name (Abs (_, _, t)) = Term.incr_boundvars ~1 (antiquote_tr' name t)

--- a/src/Pure/goal.ML	Wed Nov 09 16:26:53 2005 +0100
+++ b/src/Pure/goal.ML	Wed Nov 09 16:26:54 2005 +0100
@@ -2,7 +2,7 @@
     ID:         $Id$
     Author:     Makarius and Lawrence C Paulson
 
-Tactical goal state.
+Goals in tactical theorem proving.
 *)
 
 signature BASIC_GOAL =
@@ -21,9 +21,9 @@
   val compose_hhf: thm -> int -> thm -> thm Seq.seq
   val compose_hhf_tac: thm -> int -> tactic
   val comp_hhf: thm -> thm -> thm
-  val prove: theory -> string list -> term list -> term -> (thm list -> tactic) -> thm
   val prove_multi: theory -> string list -> term list -> term list ->
     (thm list -> tactic) -> thm list
+  val prove: theory -> string list -> term list -> term -> (thm list -> tactic) -> thm
   val prove_raw: cterm list -> cterm -> (thm list -> tactic) -> thm
 end;
 
@@ -104,9 +104,9 @@
   let
     val prop = Logic.mk_conjunction_list props;
     val statement = Logic.list_implies (asms, prop);
-    val frees = map Term.dest_Free (Term.term_frees statement);
+    val frees = Term.add_frees statement [];
     val fixed_frees = filter_out (member (op =) xs o #1) frees;
-    val fixed_tfrees = foldr Term.add_typ_tfrees [] (map #2 fixed_frees);
+    val fixed_tfrees = fold (Term.add_tfreesT o #2) fixed_frees [];
     val params = List.mapPartial (fn x => Option.map (pair x) (AList.lookup (op =) frees x)) xs;
 
     fun err msg = raise ERROR_MESSAGE
@@ -136,8 +136,8 @@
       (Drule.implies_intr_list casms
         #> Drule.forall_intr_list cparams
         #> norm_hhf
-        #> (#1 o Thm.varifyT' fixed_tfrees)
-        #> Drule.zero_var_indexes)
+        #> Thm.varifyT' fixed_tfrees
+        #-> K Drule.zero_var_indexes)
   end;
 
 

--- a/src/Pure/theory.ML	Wed Nov 09 16:26:53 2005 +0100
+++ b/src/Pure/theory.ML	Wed Nov 09 16:26:54 2005 +0100
@@ -273,8 +273,8 @@
     val show_tfrees = commas_quote o map fst;
 
     val lhs_nofrees = filter (not o can dest_free) args;
-    val lhs_dups = duplicates args;
-    val rhs_extras = term_frees rhs |> fold (remove op =) args;
+    val lhs_dups = gen_duplicates (op aconv) args;
+    val rhs_extras = term_frees rhs |> fold (remove op aconv) args;
     val rhs_extrasT = term_tfrees rhs |> fold (remove op =) (typ_tfrees T);
   in
     if not (null lhs_nofrees) then