src/HOLCF/Tools/cont_consts.ML
changeset 37098 b86d546c5282
parent 36960 01594f816e3a
child 40327 1dfdbd66093a
--- a/src/HOLCF/Tools/cont_consts.ML	Sat May 22 18:34:38 2010 -0700
+++ b/src/HOLCF/Tools/cont_consts.ML	Sat May 22 19:17:18 2010 -0700
@@ -90,11 +90,4 @@
 
 end;
 
-
-(* outer syntax *)
-
-val _ =
-  Outer_Syntax.command "consts" "declare constants (HOLCF)" Keyword.thy_decl
-    (Scan.repeat1 Parse.const_binding >> (Toplevel.theory o add_consts_cmd));
-
 end;