changeset 24867 | e5b55d7be9bb |
parent 24707 | dfeb98f84e93 |
child 30345 | 76fd85bbf139 |
--- a/src/HOLCF/Tools/cont_consts.ML Sat Oct 06 16:41:22 2007 +0200 +++ b/src/HOLCF/Tools/cont_consts.ML Sat Oct 06 16:50:04 2007 +0200 @@ -99,12 +99,10 @@ local structure P = OuterParse and K = OuterKeyword in -val constsP = +val _ = OuterSyntax.command "consts" "declare constants (HOLCF)" K.thy_decl (Scan.repeat1 P.const >> (Toplevel.theory o add_consts)); -val _ = OuterSyntax.add_parsers [constsP]; - end; end;