# HG changeset patch
# User wenzelm
# Date 932741565 -7200
# Node ID 893e5a8a8d46c026513a4d1a131e7d8d9d5fa4a2
# Parent  f54023a6c7e2ca44f1357fc551c63762a443a250
tuned add_term_varnames;

diff -r f54023a6c7e2 -r 893e5a8a8d46 src/Pure/thm.ML
--- a/src/Pure/thm.ML	Fri Jul 23 16:51:52 1999 +0200
+++ b/src/Pure/thm.ML	Fri Jul 23 16:52:45 1999 +0200
@@ -1605,6 +1605,12 @@
 
 (** simpset operations **)
 
+(* term variables *)
+
+val add_term_varnames = foldl_aterms (fn (xs, Var (x, _)) => ins_ix (x, xs) | (xs, _) => xs);
+fun term_varnames t = add_term_varnames ([], t);
+
+
 (* dest_mss *)
 
 fun dest_mss (Mss {rules, congs, procs, ...}) =
@@ -1632,6 +1638,7 @@
         generic_merge eq_prem I I prems1 prems2,
         mk_rews, termless);
 
+
 (* add_simps *)
 
 fun mk_rrule2{thm,lhs,perm} =
@@ -1654,15 +1661,14 @@
   | vperm (t, u) = (t = u);
 
 fun var_perm (t, u) =
-  vperm (t, u) andalso eq_set_term (term_vars t, term_vars u);
+  vperm (t, u) andalso eq_set (term_varnames t, term_varnames 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_vars erhs) subset
-       (union_term (term_vars elhs, List.concat(map term_vars prems))))
+  not (term_varnames erhs subset foldl add_term_varnames (term_varnames elhs, prems))
   orelse
   not ((term_tvars erhs) subset
        (term_tvars elhs  union  List.concat(map term_tvars prems)));
@@ -1705,7 +1711,7 @@
    in case there are extra vars on the rhs *)
 fun rrule_eq_True(thm,lhs,rhs,mss,thm2) =
   let val rrule = {thm=thm, lhs=lhs, perm=false}
-  in if (term_vars rhs)  subset (term_vars lhs) andalso
+  in if (term_varnames rhs)  subset (term_varnames lhs) andalso
         (term_tvars rhs) subset (term_tvars lhs)
      then [rrule]
      else mk_eq_True mss thm2 @ [rrule]
@@ -1988,7 +1994,7 @@
    while the premises are solved.
 *)
 fun cond_skel(args as (congs,(lhs,rhs))) =
-  if term_vars rhs subset term_vars lhs then uncond_skel(args)
+  if term_varnames rhs subset term_varnames lhs then uncond_skel(args)
   else skel0;
 
 (*