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