--- a/src/Pure/meta_simplifier.ML Fri Jul 15 15:44:11 2005 +0200
+++ b/src/Pure/meta_simplifier.ML Fri Jul 15 15:44:15 2005 +0200
@@ -403,7 +403,7 @@
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 Library.foldl add_term_varnames (term_varnames elhs, prems))
+ not (term_varnames erhs subset fold add_term_varnames prems (term_varnames elhs))
orelse
not (term_tvars erhs subset (term_tvars elhs union List.concat (map term_tvars prems)));