src/Pure/Isar/isar_syn.ML
changeset 35625 9c818cab0dd0
parent 35413 4c7cba1f7ce9
child 35626 06197484c6ad
     1.1 --- a/src/Pure/Isar/isar_syn.ML	Sun Mar 07 11:57:16 2010 +0100
     1.2 +++ b/src/Pure/Isar/isar_syn.ML	Sun Mar 07 12:19:47 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 (ObjectLogic.typedecl (a, args, mx) #> snd)));
     1.8 +      Toplevel.theory (Object_Logic.typedecl (a, args, mx) #> snd)));
     1.9  
    1.10  val _ =
    1.11    OuterSyntax.command "types" "declare type abbreviations" K.thy_decl
    1.12 @@ -127,7 +127,7 @@
    1.13  
    1.14  val _ =
    1.15    OuterSyntax.command "judgment" "declare object-logic judgment" K.thy_decl
    1.16 -    (P.const_binding >> (Toplevel.theory o ObjectLogic.add_judgment_cmd));
    1.17 +    (P.const_binding >> (Toplevel.theory o Object_Logic.add_judgment_cmd));
    1.18  
    1.19  val _ =
    1.20    OuterSyntax.command "consts" "declare constants" K.thy_decl