1.1 --- a/src/Pure/thm.ML	Fri Jul 23 16:51:52 1999 +0200
     1.2 +++ b/src/Pure/thm.ML	Fri Jul 23 16:52:45 1999 +0200
     1.3 @@ -1605,6 +1605,12 @@
     1.4  
     1.5  (** simpset operations **)
     1.6  
     1.7 +(* term variables *)
     1.8 +
     1.9 +val add_term_varnames = foldl_aterms (fn (xs, Var (x, _)) => ins_ix (x, xs) | (xs, _) => xs);
    1.10 +fun term_varnames t = add_term_varnames ([], t);
    1.11 +
    1.12 +
    1.13  (* dest_mss *)
    1.14  
    1.15  fun dest_mss (Mss {rules, congs, procs, ...}) =
    1.16 @@ -1632,6 +1638,7 @@
    1.17          generic_merge eq_prem I I prems1 prems2,
    1.18          mk_rews, termless);
    1.19  
    1.20 +
    1.21  (* add_simps *)
    1.22  
    1.23  fun mk_rrule2{thm,lhs,perm} =
    1.24 @@ -1654,15 +1661,14 @@
    1.25    | vperm (t, u) = (t = u);
    1.26  
    1.27  fun var_perm (t, u) =
    1.28 -  vperm (t, u) andalso eq_set_term (term_vars t, term_vars u);
    1.29 +  vperm (t, u) andalso eq_set (term_varnames t, term_varnames u);
    1.30  
    1.31  (* FIXME: it seems that the conditions on extra variables are too liberal if
    1.32  prems are nonempty: does solving the prems really guarantee instantiation of
    1.33  all its Vars? Better: a dynamic check each time a rule is applied.
    1.34  *)
    1.35  fun rewrite_rule_extra_vars prems elhs erhs =
    1.36 -  not ((term_vars erhs) subset
    1.37 -       (union_term (term_vars elhs, List.concat(map term_vars prems))))
    1.38 +  not (term_varnames erhs subset foldl add_term_varnames (term_varnames elhs, prems))
    1.39    orelse
    1.40    not ((term_tvars erhs) subset
    1.41         (term_tvars elhs  union  List.concat(map term_tvars prems)));
    1.42 @@ -1705,7 +1711,7 @@
    1.43     in case there are extra vars on the rhs *)
    1.44  fun rrule_eq_True(thm,lhs,rhs,mss,thm2) =
    1.45    let val rrule = {thm=thm, lhs=lhs, perm=false}
    1.46 -  in if (term_vars rhs)  subset (term_vars lhs) andalso
    1.47 +  in if (term_varnames rhs)  subset (term_varnames lhs) andalso
    1.48          (term_tvars rhs) subset (term_tvars lhs)
    1.49       then [rrule]
    1.50       else mk_eq_True mss thm2 @ [rrule]
    1.51 @@ -1988,7 +1994,7 @@
    1.52     while the premises are solved.
    1.53  *)
    1.54  fun cond_skel(args as (congs,(lhs,rhs))) =
    1.55 -  if term_vars rhs subset term_vars lhs then uncond_skel(args)
    1.56 +  if term_varnames rhs subset term_varnames lhs then uncond_skel(args)
    1.57    else skel0;
    1.58  
    1.59  (*