--- a/src/HOL/Import/proof_kernel.ML Tue Dec 06 06:22:14 2005 +0100
+++ b/src/HOL/Import/proof_kernel.ML Tue Dec 06 09:04:09 2005 +0100
@@ -1903,7 +1903,7 @@
Replaying _ => thy
| _ => Theory.add_consts_i [(constname,ctype,csyn)] thy
val eq = mk_defeq constname rhs' thy1
- val (thy2,thms) = PureThy.add_defs_i false [((thmname,eq),[])] thy1
+ val (thms, thy2) = PureThy.add_defs_i false [((thmname,eq),[])] thy1
val def_thm = hd thms
val thm' = def_thm RS meta_eq_to_obj_eq_thm
val (thy',th) = (thy2, thm')