src/HOLCF/Tools/cont_consts.ML
changeset 36960 01594f816e3a
parent 35525 fa231b86cb1e
child 37098 b86d546c5282
--- 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;