src/HOL/Tools/res_atp.ML
changeset 24867 e5b55d7be9bb
parent 24854 0ebcd575d3c6
child 24920 2a45e400fdad
     1.1 --- a/src/HOL/Tools/res_atp.ML	Sat Oct 06 16:41:22 2007 +0200
     1.2 +++ b/src/HOL/Tools/res_atp.ML	Sat Oct 06 16:50:04 2007 +0200
     1.3 @@ -969,8 +969,8 @@
     1.4            isar_atp_writeonly (ctxt, chain_ths, goal))
     1.5    end;
     1.6  
     1.7 -val _ = OuterSyntax.add_parsers
     1.8 -  [OuterSyntax.command "sledgehammer" "call automatic theorem provers" OuterKeyword.diag
     1.9 -    (Scan.succeed (Toplevel.no_timing o Toplevel.unknown_proof o Toplevel.keep sledgehammer))];
    1.10 +val _ =
    1.11 +  OuterSyntax.command "sledgehammer" "call automatic theorem provers" OuterKeyword.diag
    1.12 +    (Scan.succeed (Toplevel.no_timing o Toplevel.unknown_proof o Toplevel.keep sledgehammer));
    1.13  
    1.14  end;