src/HOL/Tools/datatype_package.ML
changeset 16122 864fda4a4056
parent 15704 93163972dbdc
child 16364 dc9f7066d80a
     1.1 --- a/src/HOL/Tools/datatype_package.ML	Tue May 31 11:53:12 2005 +0200
     1.2 +++ b/src/HOL/Tools/datatype_package.ML	Tue May 31 11:53:13 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.cond_extern_table sg Sign.typeK tab)));
     1.8 +      map #1 (Sign.extern_table sg Sign.typeK 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.cond_extern sg Sign.constK cname,
    1.17 +      (Sign.extern sg Sign.constK 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