src/HOL/Tools/datatype_package.ML
changeset 16364 dc9f7066d80a
parent 16122 864fda4a4056
child 16430 bc07926e4f03
     1.1 --- a/src/HOL/Tools/datatype_package.ML	Sat Jun 11 22:15:47 2005 +0200
     1.2 +++ b/src/HOL/Tools/datatype_package.ML	Sat Jun 11 22:15:48 2005 +0200
     1.3 @@ -99,7 +99,7 @@
     1.4  
     1.5    fun print sg tab =
     1.6      Pretty.writeln (Pretty.strs ("datatypes:" ::
     1.7 -      map #1 (Sign.extern_table sg Sign.typeK tab)));
     1.8 +      map #1 (NameSpace.extern_table (Sign.type_space sg, tab))));
     1.9  end;
    1.10  
    1.11  structure DatatypesData = TheoryDataFun(DatatypesArgs);
    1.12 @@ -466,7 +466,7 @@
    1.13          (loose_bnos (strip_abs_body t))
    1.14        end;
    1.15      val cases = map (fn ((cname, dts), t) =>
    1.16 -      (Sign.extern sg Sign.constK cname,
    1.17 +      (Sign.extern_const sg cname,
    1.18         strip_abs (length dts) t, is_dependent (length dts) t))
    1.19        (constrs ~~ fs);
    1.20      fun count_cases (cs, (_, _, true)) = cs