--- a/src/HOL/Import/replay.ML Thu Apr 06 16:12:57 2006 +0200
+++ b/src/HOL/Import/replay.ML Thu Apr 06 16:13:17 2006 +0200
@@ -344,7 +344,7 @@
| delta (Hol_theorem (thyname, thmname, th)) thy =
add_hol4_theorem thyname thmname ([], th_of thy th) thy
| delta (Typedef (thmname, typ, c, repabs, th)) thy =
- fst(TypedefPackage.add_typedef_i false thmname typ c repabs (rtac (th_of thy th) 1) thy)
+ snd (TypedefPackage.add_typedef_i false thmname typ c repabs (rtac (th_of thy th) 1) thy)
| delta (Hol_type_mapping (thyname, tycname, fulltyname)) thy =
add_hol4_type_mapping thyname tycname true fulltyname thy
| delta (Indexed_theorem (i, th)) thy =