--- a/src/HOL/Tools/datatype_package.ML Wed Nov 28 16:44:18 2007 +0100
+++ b/src/HOL/Tools/datatype_package.ML Wed Nov 28 16:44:20 2007 +0100
@@ -557,7 +557,7 @@
val thy2' = thy
(** new types **)
- |> fold2 (fn (name, mx) => fn tvs => Typedecl.add (name, tvs, mx) #> snd)
+ |> fold2 (fn (name, mx) => fn tvs => ObjectLogic.typedecl (name, tvs, mx) #> snd)
types_syntax tyvars
|> add_path flat_names (space_implode "_" new_type_names)
--- a/src/HOL/Tools/typedef_package.ML Wed Nov 28 16:44:18 2007 +0100
+++ b/src/HOL/Tools/typedef_package.ML Wed Nov 28 16:44:20 2007 +0100
@@ -135,7 +135,7 @@
else (NONE, thy);
fun typedef_result nonempty =
- Typedecl.add (t, vs, mx)
+ ObjectLogic.typedecl (t, vs, mx)
#> snd
#> Sign.add_consts_i
((if def then [(name, setT', NoSyn)] else []) @
--- a/src/Pure/Isar/isar_syn.ML Wed Nov 28 16:44:18 2007 +0100
+++ b/src/Pure/Isar/isar_syn.ML Wed Nov 28 16:44:20 2007 +0100
@@ -113,7 +113,7 @@
val _ =
OuterSyntax.command "typedecl" "type declaration" K.thy_decl
(P.type_args -- P.name -- P.opt_infix >> (fn ((args, a), mx) =>
- Toplevel.theory (Typedecl.add (a, args, mx) #> snd)));
+ Toplevel.theory (ObjectLogic.typedecl (a, args, mx) #> snd)));
val _ =
OuterSyntax.command "types" "declare type abbreviations" K.thy_decl