--- 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;