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