--- 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