# HG changeset patch
# User wenzelm
# Date 1118520947 -7200
# Node ID c686a606dfbaa822ba1da06d3baa053d26a98fc2
# Parent  f321def7279ce733ffcf73b2d537b8be79d0fe5d
renamed Sign.intern_tycon to Sign.intern_type;

diff -r f321def7279c -r c686a606dfba src/HOL/Import/proof_kernel.ML
--- a/src/HOL/Import/proof_kernel.ML	Sat Jun 11 15:42:51 2005 +0200
+++ b/src/HOL/Import/proof_kernel.ML	Sat Jun 11 22:15:47 2005 +0200
@@ -2046,7 +2046,7 @@
 				      
 	    val th3 = (#type_definition typedef_info) RS typedef_hol2hol4
 
-	    val fulltyname = Sign.intern_tycon (sign_of thy') tycname
+	    val fulltyname = Sign.intern_type (sign_of thy') tycname
 	    val thy'' = add_hol4_type_mapping thyname tycname true fulltyname thy'
 
 	    val sg = sign_of thy''
@@ -2110,7 +2110,7 @@
 	    val th3 = (#type_definition typedef_info) RS typedef_hol2hollight
 
 	    val th4 = Drule.freeze_all th3
-	    val fulltyname = Sign.intern_tycon (sign_of thy') tycname
+	    val fulltyname = Sign.intern_type (sign_of thy') tycname
 	    val thy'' = add_hol4_type_mapping thyname tycname true fulltyname thy'
 
 	    val sg = sign_of thy''
diff -r f321def7279c -r c686a606dfba src/Pure/Proof/extraction.ML
--- a/src/Pure/Proof/extraction.ML	Sat Jun 11 15:42:51 2005 +0200
+++ b/src/Pure/Proof/extraction.ML	Sat Jun 11 22:15:47 2005 +0200
@@ -403,7 +403,7 @@
   in
     ExtractionData.put
       {realizes_eqns = realizes_eqns, typeof_eqns = typeof_eqns,
-       types = map (apfst (Sign.intern_tycon (sign_of thy))) tys @ types,
+       types = map (apfst (Sign.intern_type (sign_of thy))) tys @ types,
        realizers = realizers, defs = defs, expand = expand, prep = prep} thy
   end;