HOLCF no longer redefines 'consts' command
authorhuffman
Sat, 22 May 2010 19:17:18 -0700
changeset 37098 b86d546c5282
parent 37097 476016cbf8b3
child 37099 3636b08cbf51
HOLCF no longer redefines 'consts' command
src/HOLCF/Tools/cont_consts.ML
--- 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;