diff -r f5417836dbea -r 01594f816e3a src/HOLCF/Tools/cont_consts.ML
--- 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;