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/local_defs.ML
changeset 22568 ed7aa5a350ef
parent 21844 e10b8bd7a886
child 22671 3c62305fbee6 
--- a/src/Pure/Isar/local_defs.ML	Tue Apr 03 19:24:11 2007 +0200
+++ b/src/Pure/Isar/local_defs.ML	Tue Apr 03 19:24:13 2007 +0200
@@ -124,7 +124,7 @@
       (case filter_out is_trivial raw_eqs of
         [] => th
       | eqs =>
-          let val ((_, th' :: eqs'), ctxt') = Variable.import true (th :: eqs) ctxt
+          let val ((_, th' :: eqs'), ctxt') = Variable.import_thms true (th :: eqs) ctxt
           in singleton (Variable.export ctxt' ctxt) (fold trans eqs' th') end);
 
 in
isabelle