# HG changeset patch
# User obua
# Date 1127508565 -7200
# Node ID 73397145d58a732723ed55e2b781f3ea9965994d
# Parent  f526e2b9fe9ed0c3bef79af984e40403d81e8187
fix

diff -r f526e2b9fe9e -r 73397145d58a src/HOL/Import/proof_kernel.ML
--- 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