--- a/src/HOL/Import/proof_kernel.ML Fri Sep 23 22:31:22 2005 +0200
+++ b/src/HOL/Import/proof_kernel.ML Fri Sep 23 22:49:25 2005 +0200
@@ -2114,7 +2114,7 @@
val tnames = sort string_ord (map fst tfrees)
val tsyn = mk_syn thy tycname
val typ = (tycname,tnames,tsyn)
- val (thy',typedef_info) = TypedefPackage.add_typedef_i false (SOME thmname) typ c (SOME(rep_name,abs_name)) (rtac th2 1) thy
+ val (thy',typedef_info) = TypedefPackage.add_typedef_i false NONE typ c (SOME(rep_name,abs_name)) (rtac th2 1) thy
val fulltyname = Sign.intern_type (sign_of thy') tycname
val aty = Type (fulltyname, map mk_vartype tnames)
val abs_ty = tT --> aty