use Term.add_vars instead of obsolete term_varnames;
authorwenzelm
Tue Jul 25 21:18:04 2006 +0200 (2006-07-25)
changeset 20197ffc64d90fc1f
parent 20196 9a19e4de6e2e
child 20198 7b385487f22f
use Term.add_vars instead of obsolete term_varnames;
src/HOL/Tools/ATP/reduce_axiomsN.ML
src/Pure/meta_simplifier.ML
     1.1 --- a/src/HOL/Tools/ATP/reduce_axiomsN.ML	Tue Jul 25 21:18:02 2006 +0200
     1.2 +++ b/src/HOL/Tools/ATP/reduce_axiomsN.ML	Tue Jul 25 21:18:04 2006 +0200
     1.3 @@ -158,7 +158,7 @@
     1.4              let val (rator,args) = strip_comb lhs
     1.5  		val ct = const_with_typ thy (dest_ConstFree rator)
     1.6              in  forall is_Var args andalso uni_mem gctypes ct andalso
     1.7 -                term_varnames rhs subset term_varnames lhs
     1.8 +                Term.add_vars rhs [] subset Term.add_vars lhs []
     1.9              end
    1.10  	    handle ConstFree => false
    1.11      in    
    1.12 @@ -205,4 +205,4 @@
    1.13    else map #1 (relevance_filter_aux thy axioms goals);
    1.14      
    1.15  
    1.16 -end;
    1.17 \ No newline at end of file
    1.18 +end;
     2.1 --- a/src/Pure/meta_simplifier.ML	Tue Jul 25 21:18:02 2006 +0200
     2.2 +++ b/src/Pure/meta_simplifier.ML	Tue Jul 25 21:18:04 2006 +0200
     2.3 @@ -397,14 +397,14 @@
     2.4    | vperm (t, u) = (t = u);
     2.5  
     2.6  fun var_perm (t, u) =
     2.7 -  vperm (t, u) andalso gen_eq_set (op =) (term_varnames t, term_varnames u);
     2.8 +  vperm (t, u) andalso gen_eq_set (op =) (Term.add_vars t [], Term.add_vars u []);
     2.9  
    2.10  (* FIXME: it seems that the conditions on extra variables are too liberal if
    2.11  prems are nonempty: does solving the prems really guarantee instantiation of
    2.12  all its Vars? Better: a dynamic check each time a rule is applied.
    2.13  *)
    2.14  fun rewrite_rule_extra_vars prems elhs erhs =
    2.15 -  not (term_varnames erhs subset fold add_term_varnames prems (term_varnames elhs))
    2.16 +  not (Term.add_vars erhs [] subset fold Term.add_vars (elhs :: prems) [])
    2.17    orelse
    2.18    not (term_tvars erhs subset (term_tvars elhs union maps term_tvars prems));
    2.19  
    2.20 @@ -462,7 +462,7 @@
    2.21    in case there are extra vars on the rhs*)
    2.22  fun rrule_eq_True (thm, name, lhs, elhs, rhs, ss, thm2) =
    2.23    let val rrule = {thm = thm, name = name, lhs = lhs, elhs = elhs, perm = false} in
    2.24 -    if term_varnames rhs subset term_varnames lhs andalso
    2.25 +    if Term.add_vars rhs [] subset Term.add_vars lhs [] andalso
    2.26        term_tvars rhs subset term_tvars lhs then [rrule]
    2.27      else mk_eq_True ss (thm2, name) @ [rrule]
    2.28    end;
    2.29 @@ -811,7 +811,7 @@
    2.30    while the premises are solved.*)
    2.31  
    2.32  fun cond_skel (args as (congs, (lhs, rhs))) =
    2.33 -  if term_varnames rhs subset term_varnames lhs then uncond_skel args
    2.34 +  if Term.add_vars rhs [] subset Term.add_vars lhs [] then uncond_skel args
    2.35    else skel0;
    2.36  
    2.37  (*