Mercurial Mercurial > repos > isabelle / diff
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | file | latest | revisions | annotate | diff | comparison | raw | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
src/Pure/Isar/obtain.ML
changeset 19300 7689f81f8996
parent 18907 f984f22f1cb4
child 19482 9f11af8f7ef9 
--- a/src/Pure/Isar/obtain.ML	Tue Mar 21 12:18:06 2006 +0100
+++ b/src/Pure/Isar/obtain.ML	Tue Mar 21 12:18:07 2006 +0100
@@ -208,7 +208,7 @@
     val rule' = rule |> Thm.instantiate (instT, []);
 
     val tvars = Drule.tvars_of rule';
-    val vars = fold (remove op =) (Term.add_vars (Thm.concl_of rule') []) (Drule.vars_of rule');
+    val vars = subtract (op =) (Term.add_vars (Thm.concl_of rule') []) (Drule.vars_of rule');
     val _ =
       if null tvars andalso null vars then ()
       else err ("Illegal schematic variable(s) " ^
isabelle