src/HOL/Import/proof_kernel.ML
changeset 28662 64ab5bb68d4c
parent 28397 389c5e494605
child 28677 4693938e9c2a
     1.1 --- a/src/HOL/Import/proof_kernel.ML	Wed Oct 22 14:15:43 2008 +0200
     1.2 +++ b/src/HOL/Import/proof_kernel.ML	Wed Oct 22 14:15:44 2008 +0200
     1.3 @@ -2097,7 +2097,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 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 @@ -2183,7 +2183,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 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)