diff -r c5030cdbf8da -r 0a733e11021a src/HOL/Import/proof_kernel.ML
--- 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')