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 31794 71af1fd6a5e4
parent 30763 6976521b4263
child 32091 30e2ffbba718 
--- a/src/Pure/Isar/local_defs.ML	Wed Jun 24 20:52:49 2009 +0200
+++ b/src/Pure/Isar/local_defs.ML	Wed Jun 24 21:28:02 2009 +0200
@@ -170,7 +170,7 @@
       (case filter_out is_trivial raw_eqs of
         [] => th
       | eqs =>
-          let val ((_, th' :: eqs'), ctxt') = Variable.import_thms true (th :: eqs) ctxt
+          let val ((_, th' :: eqs'), ctxt') = Variable.import true (th :: eqs) ctxt
           in singleton (Variable.export ctxt' ctxt) (fold trans eqs' th') end);
 
 in
isabelle