src/Pure/Isar/isar_syn.ML
changeset 35626 06197484c6ad
parent 35625 9c818cab0dd0
child 35681 8b22a498b034
--- a/src/Pure/Isar/isar_syn.ML	Sun Mar 07 12:19:47 2010 +0100
+++ b/src/Pure/Isar/isar_syn.ML	Sun Mar 07 12:47:02 2010 +0100
@@ -105,7 +105,7 @@
 val _ =
   OuterSyntax.command "typedecl" "type declaration" K.thy_decl
     (P.type_args -- P.binding -- P.opt_mixfix >> (fn ((args, a), mx) =>
-      Toplevel.theory (Object_Logic.typedecl (a, args, mx) #> snd)));
+      Toplevel.theory (Typedecl.typedecl (a, args, mx) #> snd)));
 
 val _ =
   OuterSyntax.command "types" "declare type abbreviations" K.thy_decl