# HG changeset patch
# User wenzelm
# Date 1153855084 -7200
# Node ID ffc64d90fc1f06842cd135dcff20aebcefbf16dd
# Parent  9a19e4de6e2e87e105d002be6341b60df62d2448
use Term.add_vars instead of obsolete term_varnames;

diff -r 9a19e4de6e2e -r ffc64d90fc1f src/HOL/Tools/ATP/reduce_axiomsN.ML
--- a/src/HOL/Tools/ATP/reduce_axiomsN.ML	Tue Jul 25 21:18:02 2006 +0200
+++ b/src/HOL/Tools/ATP/reduce_axiomsN.ML	Tue Jul 25 21:18:04 2006 +0200
@@ -158,7 +158,7 @@
             let val (rator,args) = strip_comb lhs
 		val ct = const_with_typ thy (dest_ConstFree rator)
             in  forall is_Var args andalso uni_mem gctypes ct andalso
-                term_varnames rhs subset term_varnames lhs
+                Term.add_vars rhs [] subset Term.add_vars lhs []
             end
 	    handle ConstFree => false
     in    
@@ -205,4 +205,4 @@
   else map #1 (relevance_filter_aux thy axioms goals);
     
 
-end;
\ No newline at end of file
+end;
diff -r 9a19e4de6e2e -r ffc64d90fc1f src/Pure/meta_simplifier.ML
--- a/src/Pure/meta_simplifier.ML	Tue Jul 25 21:18:02 2006 +0200
+++ b/src/Pure/meta_simplifier.ML	Tue Jul 25 21:18:04 2006 +0200
@@ -397,14 +397,14 @@
   | vperm (t, u) = (t = u);
 
 fun var_perm (t, u) =
-  vperm (t, u) andalso gen_eq_set (op =) (term_varnames t, term_varnames u);
+  vperm (t, u) andalso gen_eq_set (op =) (Term.add_vars t [], Term.add_vars u []);
 
 (* FIXME: it seems that the conditions on extra variables are too liberal if
 prems are nonempty: does solving the prems really guarantee instantiation of
 all its Vars? Better: a dynamic check each time a rule is applied.
 *)
 fun rewrite_rule_extra_vars prems elhs erhs =
-  not (term_varnames erhs subset fold add_term_varnames prems (term_varnames elhs))
+  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));
 
@@ -462,7 +462,7 @@
   in case there are extra vars on the rhs*)
 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_varnames rhs subset term_varnames lhs andalso
+    if Term.add_vars rhs [] subset Term.add_vars lhs [] andalso
       term_tvars rhs subset term_tvars lhs then [rrule]
     else mk_eq_True ss (thm2, name) @ [rrule]
   end;
@@ -811,7 +811,7 @@
   while the premises are solved.*)
 
 fun cond_skel (args as (congs, (lhs, rhs))) =
-  if term_varnames rhs subset term_varnames lhs then uncond_skel args
+  if Term.add_vars rhs [] subset Term.add_vars lhs [] then uncond_skel args
   else skel0;
 
 (*