--- a/src/HOLCF/Tools/cont_consts.ML Mon May 17 15:11:25 2010 +0200
+++ b/src/HOLCF/Tools/cont_consts.ML Mon May 17 23:54:15 2010 +0200
@@ -93,12 +93,8 @@
(* outer syntax *)
-local structure P = OuterParse and K = OuterKeyword in
-
val _ =
- OuterSyntax.command "consts" "declare constants (HOLCF)" K.thy_decl
- (Scan.repeat1 P.const_binding >> (Toplevel.theory o add_consts_cmd));
+ Outer_Syntax.command "consts" "declare constants (HOLCF)" Keyword.thy_decl
+ (Scan.repeat1 Parse.const_binding >> (Toplevel.theory o add_consts_cmd));
end;
-
-end;