src/HOL/Import/proof_kernel.ML
changeset 20483 04aa552a83bc
parent 20286 4cf8e86a2d29
child 20854 f9cf9e62d11c
     1.1 --- a/src/HOL/Import/proof_kernel.ML	Tue Sep 05 22:06:18 2006 +0200
     1.2 +++ b/src/HOL/Import/proof_kernel.ML	Wed Sep 06 10:01:04 2006 +0200
     1.3 @@ -2094,7 +2094,7 @@
     1.4  	    val tnames = map fst tfrees
     1.5  	    val tsyn = mk_syn thy tycname
     1.6  	    val typ = (tycname,tnames,tsyn)
     1.7 -	    val (typedef_info, thy') = TypedefPackage.add_typedef_i false (SOME thmname) typ c NONE (rtac th2 1) thy	    
     1.8 +	    val ((_, typedef_info), thy') = TypedefPackage.add_typedef_i false (SOME thmname) typ c NONE (rtac th2 1) thy	    
     1.9              val _ = ImportRecorder.add_typedef (SOME thmname) typ c NONE th2
    1.10  				      
    1.11  	    val th3 = (#type_definition typedef_info) RS typedef_hol2hol4
    1.12 @@ -2187,7 +2187,7 @@
    1.13  	    val tnames = sort string_ord (map fst tfrees)
    1.14  	    val tsyn = mk_syn thy tycname
    1.15  	    val typ = (tycname,tnames,tsyn)
    1.16 -	    val (typedef_info, thy') = TypedefPackage.add_typedef_i false NONE typ c (SOME(rep_name,abs_name)) (rtac th2 1) thy
    1.17 +	    val ((_, typedef_info), thy') = TypedefPackage.add_typedef_i false NONE typ c (SOME(rep_name,abs_name)) (rtac th2 1) thy
    1.18  	    val _ = ImportRecorder.add_typedef NONE typ c (SOME(rep_name,abs_name)) th2
    1.19  	    val fulltyname = Sign.intern_type thy' tycname
    1.20  	    val aty = Type (fulltyname, map mk_vartype tnames)