src/HOL/Import/proof_kernel.ML
changeset 30346 90efbb8a8cb2
parent 30190 479806475f3c
child 30447 955190fa639b
     1.1 --- a/src/HOL/Import/proof_kernel.ML	Sat Mar 07 22:17:25 2009 +0100
     1.2 +++ b/src/HOL/Import/proof_kernel.ML	Sat Mar 07 23:30:58 2009 +0100
     1.3 @@ -1926,7 +1926,8 @@
     1.4          val csyn = mk_syn thy constname
     1.5          val thy1 = case HOL4DefThy.get thy of
     1.6                         Replaying _ => thy
     1.7 -                     | _ => (ImportRecorder.add_consts [(constname, ctype, csyn)]; Sign.add_consts_i [(constname,ctype,csyn)] thy)
     1.8 +                     | _ => (ImportRecorder.add_consts [(constname, ctype, csyn)];
     1.9 +                              Sign.add_consts_i [(Binding.name constname,ctype,csyn)] thy)
    1.10          val eq = mk_defeq constname rhs' thy1
    1.11          val (thms, thy2) = PureThy.add_defs false [((Binding.name thmname,eq),[])] thy1
    1.12          val _ = ImportRecorder.add_defs thmname eq
    1.13 @@ -2017,7 +2018,7 @@
    1.14                                 val thy' = add_dump str thy
    1.15                                 val _ = ImportRecorder.add_consts consts
    1.16                             in
    1.17 -                               Sign.add_consts_i consts thy'
    1.18 +                               Sign.add_consts_i (map (fn (c, T, mx) => (Binding.name c, T, mx)) consts) thy'
    1.19                             end
    1.20  
    1.21              val thy1 = List.foldr (fn(name,thy)=>
    1.22 @@ -2093,7 +2094,9 @@
    1.23              val tnames = map fst tfrees
    1.24              val tsyn = mk_syn thy tycname
    1.25              val typ = (tycname,tnames,tsyn)
    1.26 -            val ((_, typedef_info), thy') = TypedefPackage.add_typedef false (SOME thmname) typ c NONE (rtac th2 1) thy
    1.27 +            val ((_, typedef_info), thy') =
    1.28 +              TypedefPackage.add_typedef false (SOME (Binding.name thmname))
    1.29 +                (Binding.name tycname, tnames, tsyn) c NONE (rtac th2 1) thy
    1.30              val _ = ImportRecorder.add_typedef (SOME thmname) typ c NONE th2
    1.31  
    1.32              val th3 = (#type_definition typedef_info) RS typedef_hol2hol4
    1.33 @@ -2179,7 +2182,9 @@
    1.34              val tnames = sort string_ord (map fst tfrees)
    1.35              val tsyn = mk_syn thy tycname
    1.36              val typ = (tycname,tnames,tsyn)
    1.37 -            val ((_, typedef_info), thy') = TypedefPackage.add_typedef false NONE typ c (SOME(rep_name,abs_name)) (rtac th2 1) thy
    1.38 +            val ((_, typedef_info), thy') =
    1.39 +              TypedefPackage.add_typedef false NONE (Binding.name tycname,tnames,tsyn) c
    1.40 +                (SOME(Binding.name rep_name,Binding.name abs_name)) (rtac th2 1) thy
    1.41              val _ = ImportRecorder.add_typedef NONE typ c (SOME(rep_name,abs_name)) th2
    1.42              val fulltyname = Sign.intern_type thy' tycname
    1.43              val aty = Type (fulltyname, map mk_vartype tnames)