author | huffman |
Sat, 22 May 2010 19:17:18 -0700 | |
changeset 37098 | b86d546c5282 |
parent 37097 | 476016cbf8b3 |
child 37099 | 3636b08cbf51 |
--- 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;