# HG changeset patch
# User huffman
# Date 1274581038 25200
# Node ID b86d546c528214e88c80deef397924ed8f3d267a
# Parent  476016cbf8b31c7427cd9f55fdfcfb9590b6ca9c
HOLCF no longer redefines 'consts' command

diff -r 476016cbf8b3 -r b86d546c5282 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;