--- a/src/Pure/Isar/isar_syn.ML Sun Mar 07 11:57:16 2010 +0100
+++ b/src/Pure/Isar/isar_syn.ML Sun Mar 07 12:19:47 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 (ObjectLogic.typedecl (a, args, mx) #> snd)));
+ Toplevel.theory (Object_Logic.typedecl (a, args, mx) #> snd)));
val _ =
OuterSyntax.command "types" "declare type abbreviations" K.thy_decl
@@ -127,7 +127,7 @@
val _ =
OuterSyntax.command "judgment" "declare object-logic judgment" K.thy_decl
- (P.const_binding >> (Toplevel.theory o ObjectLogic.add_judgment_cmd));
+ (P.const_binding >> (Toplevel.theory o Object_Logic.add_judgment_cmd));
val _ =
OuterSyntax.command "consts" "declare constants" K.thy_decl