tuned;

--- a/src/Pure/Isar/proof_context.ML	Thu Aug 03 17:30:37 2006 +0200
+++ b/src/Pure/Isar/proof_context.ML	Thu Aug 03 17:30:38 2006 +0200
@@ -579,7 +579,7 @@
 
 in
 
-fun drop_schematic (b as (xi, SOME t)) = if null (Term.term_vars t) then b else (xi, NONE)
+fun drop_schematic (b as (xi, SOME t)) = if Term.exists_subterm is_Var t then (xi, NONE) else b
   | drop_schematic b = b;
 
 val add_binds = fold (gen_bind read_term);

--- a/src/Pure/meta_simplifier.ML	Thu Aug 03 17:30:37 2006 +0200
+++ b/src/Pure/meta_simplifier.ML	Thu Aug 03 17:30:38 2006 +0200
@@ -408,7 +408,7 @@
 fun rewrite_rule_extra_vars prems elhs erhs =
   not (Term.add_vars erhs [] subset fold Term.add_vars (elhs :: prems) [])
   orelse
-  not (term_tvars erhs subset (term_tvars elhs union maps term_tvars prems));
+  not (Term.add_tvars erhs [] subset (fold Term.add_tvars (elhs :: prems) []));
 
 (*simple test for looping rewrite rules and stupid orientations*)
 fun default_reorient thy prems lhs rhs =
@@ -465,7 +465,7 @@
 fun rrule_eq_True (thm, name, lhs, elhs, rhs, ss, thm2) =
   let val rrule = {thm = thm, name = name, lhs = lhs, elhs = elhs, perm = false} in
     if Term.add_vars rhs [] subset Term.add_vars lhs [] andalso
-      term_tvars rhs subset term_tvars lhs then [rrule]
+      Term.add_tvars rhs [] subset Term.add_tvars lhs [] then [rrule]
     else mk_eq_True ss (thm2, name) @ [rrule]
   end;
 

--- a/src/Pure/sign.ML	Thu Aug 03 17:30:37 2006 +0200
+++ b/src/Pure/sign.ML	Thu Aug 03 17:30:38 2006 +0200
@@ -481,11 +481,11 @@
 (* specifications *)
 
 fun no_vars pp tm =
-  (case (Term.term_vars tm, Term.term_tvars tm) of
+  (case (Term.add_vars tm [], Term.add_tvars tm []) of
     ([], []) => tm
-  | (ts, ixns) => error (Pretty.string_of (Pretty.block (Pretty.breaks
+  | (vars, tvars) => error (Pretty.string_of (Pretty.block (Pretty.breaks
       (Pretty.str "Illegal schematic variable(s) in term:" ::
-       map (Pretty.term pp) ts @ map (Pretty.typ pp o TVar) ixns)))));
+       map (Pretty.term pp o Var) vars @ map (Pretty.typ pp o TVar) tvars)))));
 
 fun cert_def pp tm =
   let val ((lhs, rhs), _) = tm

--- a/src/Pure/thm.ML	Thu Aug 03 17:30:37 2006 +0200
+++ b/src/Pure/thm.ML	Thu Aug 03 17:30:38 2006 +0200
@@ -1346,7 +1346,7 @@
     val newnames =
       if short < 0 then error "More names than abstractions!"
       else Name.variant_list cs (Library.take (short, iparams)) @ cs;
-    val freenames = map (#1 o dest_Free) (term_frees Bi);
+    val freenames = Term.fold_aterms (fn Free (x, _) => insert (op =) x | _ => I) Bi [];
     val newBi = Logic.list_rename_params (newnames, Bi);
   in
     case findrep cs of
@@ -1395,21 +1395,25 @@
   Preserves unknowns in tpairs and on lhs of dpairs. *)
 fun rename_bvs([],_,_,_) = I
   | rename_bvs(al,dpairs,tpairs,B) =
-    let val vars = foldr add_term_vars []
-                        (map fst dpairs @ map fst tpairs @ map snd tpairs)
+      let
+        val add_var = fold_aterms (fn Var ((x, _), _) => insert (op =) x | _ => I);
+        val vids = []
+          |> fold (add_var o fst) dpairs
+          |> fold (add_var o fst) tpairs
+          |> fold (add_var o snd) tpairs;
         (*unknowns appearing elsewhere be preserved!*)
-        val vids = map (#1 o #1 o dest_Var) vars;
         fun rename(t as Var((x,i),T)) =
-                (case AList.lookup (op =) al x of
-                   SOME(y) => if x mem_string vids orelse y mem_string vids then t
-                              else Var((y,i),T)
-                 | NONE=> t)
+              (case AList.lookup (op =) al x of
+                SOME y =>
+                  if member (op =) vids x orelse member (op =) vids y then t
+                  else Var((y,i),T)
+              | NONE=> t)
           | rename(Abs(x,T,t)) =
               Abs (the_default x (AList.lookup (op =) al x), T, rename t)
           | rename(f$t) = rename f $ rename t
           | rename(t) = t;
         fun strip_ren Ai = strip_apply rename (Ai,B)
-    in strip_ren end;
+      in strip_ren end;
 
 (*Function to rename bounds/unknowns in the argument, lifted over B*)
 fun rename_bvars(dpairs, tpairs, B) =