src/HOLCF/Tools/cont_consts.ML
changeset 24867 e5b55d7be9bb
parent 24707 dfeb98f84e93
child 30345 76fd85bbf139
--- a/src/HOLCF/Tools/cont_consts.ML	Sat Oct 06 16:41:22 2007 +0200
+++ b/src/HOLCF/Tools/cont_consts.ML	Sat Oct 06 16:50:04 2007 +0200
@@ -99,12 +99,10 @@
 
 local structure P = OuterParse and K = OuterKeyword in
 
-val constsP =
+val _ =
   OuterSyntax.command "consts" "declare constants (HOLCF)" K.thy_decl
     (Scan.repeat1 P.const >> (Toplevel.theory o add_consts));
 
-val _ = OuterSyntax.add_parsers [constsP];
-
 end;
 
 end;