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;