# HG changeset patch
# User wenzelm
# Date 1196264660 -3600
# Node ID 98f3596bec4474039aa9c8560c24b14fb654986b
# Parent  b2484a7912ac2190736e31f8c0c7116620f78c85
ObjectLogic.typedecl;

diff -r b2484a7912ac -r 98f3596bec44 src/HOL/Tools/datatype_package.ML
--- 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)
 
diff -r b2484a7912ac -r 98f3596bec44 src/HOL/Tools/typedef_package.ML
--- 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 []) @
diff -r b2484a7912ac -r 98f3596bec44 src/Pure/Isar/isar_syn.ML
--- 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