diff -r 7c10b13d49fe -r 71af1fd6a5e4 src/Pure/Isar/local_defs.ML
--- 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