diff -r 24738db98d34 -r ce171cbd4b93 src/HOL/Import/proof_kernel.ML
--- a/src/HOL/Import/proof_kernel.ML	Tue Jul 29 08:15:39 2008 +0200
+++ b/src/HOL/Import/proof_kernel.ML	Tue Jul 29 08:15:40 2008 +0200
@@ -1932,7 +1932,7 @@
                        Replaying _ => thy
                      | _ => (ImportRecorder.add_consts [(constname, ctype, csyn)]; Sign.add_consts_i [(constname,ctype,csyn)] thy)
         val eq = mk_defeq constname rhs' thy1
-        val (thms, thy2) = PureThy.add_defs_i false [((thmname,eq),[])] thy1
+        val (thms, thy2) = PureThy.add_defs false [((thmname,eq),[])] thy1
         val _ = ImportRecorder.add_defs thmname eq
         val def_thm = hd thms
         val thm' = def_thm RS meta_eq_to_obj_eq_thm