renamed Sign.intern_tycon to Sign.intern_type;
authorwenzelm
Sat Jun 11 22:15:47 2005 +0200 (2005-06-11)
changeset 16363c686a606dfba
parent 16362 f321def7279c
child 16364 dc9f7066d80a
renamed Sign.intern_tycon to Sign.intern_type;
src/HOL/Import/proof_kernel.ML
src/Pure/Proof/extraction.ML
     1.1 --- a/src/HOL/Import/proof_kernel.ML	Sat Jun 11 15:42:51 2005 +0200
     1.2 +++ b/src/HOL/Import/proof_kernel.ML	Sat Jun 11 22:15:47 2005 +0200
     1.3 @@ -2046,7 +2046,7 @@
     1.4  				      
     1.5  	    val th3 = (#type_definition typedef_info) RS typedef_hol2hol4
     1.6  
     1.7 -	    val fulltyname = Sign.intern_tycon (sign_of thy') tycname
     1.8 +	    val fulltyname = Sign.intern_type (sign_of thy') tycname
     1.9  	    val thy'' = add_hol4_type_mapping thyname tycname true fulltyname thy'
    1.10  
    1.11  	    val sg = sign_of thy''
    1.12 @@ -2110,7 +2110,7 @@
    1.13  	    val th3 = (#type_definition typedef_info) RS typedef_hol2hollight
    1.14  
    1.15  	    val th4 = Drule.freeze_all th3
    1.16 -	    val fulltyname = Sign.intern_tycon (sign_of thy') tycname
    1.17 +	    val fulltyname = Sign.intern_type (sign_of thy') tycname
    1.18  	    val thy'' = add_hol4_type_mapping thyname tycname true fulltyname thy'
    1.19  
    1.20  	    val sg = sign_of thy''
     2.1 --- a/src/Pure/Proof/extraction.ML	Sat Jun 11 15:42:51 2005 +0200
     2.2 +++ b/src/Pure/Proof/extraction.ML	Sat Jun 11 22:15:47 2005 +0200
     2.3 @@ -403,7 +403,7 @@
     2.4    in
     2.5      ExtractionData.put
     2.6        {realizes_eqns = realizes_eqns, typeof_eqns = typeof_eqns,
     2.7 -       types = map (apfst (Sign.intern_tycon (sign_of thy))) tys @ types,
     2.8 +       types = map (apfst (Sign.intern_type (sign_of thy))) tys @ types,
     2.9         realizers = realizers, defs = defs, expand = expand, prep = prep} thy
    2.10    end;
    2.11