# HG changeset patch
# User wenzelm
# Date 1178629290 -7200
# Node ID da52c2bd66ae26bd5b83a22f1dafc687099b2225
# Parent  e2511e6e5cbb5e916359f8923466358f8a56cc24
renamed call_atp to sledgehammer;

diff -r e2511e6e5cbb -r da52c2bd66ae src/HOL/Tools/res_atp.ML
--- a/src/HOL/Tools/res_atp.ML	Tue May 08 15:01:29 2007 +0200
+++ b/src/HOL/Tools/res_atp.ML	Tue May 08 15:01:30 2007 +0200
@@ -5,7 +5,6 @@
 ATPs with TPTP format input.
 *)
 
-(*Currently unused, during debugging*)
 signature RES_ATP =
 sig
   val prover: string ref
@@ -48,7 +47,7 @@
   val is_fol_thms : thm list -> bool
 end;
 
-structure ResAtp =
+structure ResAtp: RES_ATP =
 struct
 
 fun timestamp s = Output.debug (fn () => ("At " ^ Time.toString (Time.now()) ^ ": " ^ s));
@@ -508,7 +507,7 @@
 
 fun all_valid_thms ctxt =
   let
-    val banned_tab = foldl setinsert Symtab.empty (!blacklist) 
+    val banned_tab = foldl setinsert Symtab.empty (!blacklist)
     fun blacklisted s = !run_blacklist_filter andalso
                         (isSome (Symtab.lookup banned_tab s) orelse is_package_def s)
 
@@ -712,7 +711,7 @@
                           | Fol => FOL
                           | Hol => HOL
         val (included_thms,user_rules) = get_clasimp_atp_lemmas ctxt user_thms
-        val cla_simp_atp_clauses = included_thms 
+        val cla_simp_atp_clauses = included_thms
                                      |> ResAxioms.cnf_rules_pairs |> make_unique
                                      |> restrict_to_logic thy logic
                                      |> remove_unwanted_clauses
@@ -813,7 +812,7 @@
       val _ = Output.debug (fn () => "number of subgoals = " ^ Int.toString (length goals))
       val thy = ProofContext.theory_of ctxt
       fun get_neg_subgoals [] _ = []
-        | get_neg_subgoals (gl::gls) n = #1 (ResAxioms.neg_conjecture_clauses th n) :: 
+        | get_neg_subgoals (gl::gls) n = #1 (ResAxioms.neg_conjecture_clauses th n) ::
                                          get_neg_subgoals gls (n+1)
       val goal_cls = get_neg_subgoals goals 1
       val logic = case !linkup_logic_mode of
@@ -902,10 +901,12 @@
          in ignore (write_problem_files probfile (ctxt,th)) end);
 
 
-(** the Isar toplevel hook **)
+(** the Isar toplevel command **)
 
-fun invoke_atp_ml (ctxt, goal) =
-  let val thy = ProofContext.theory_of ctxt;
+fun sledgehammer state =
+  let
+    val (ctxt, (_, goal)) = Proof.get_goal (Toplevel.proof_of state);
+    val thy = ProofContext.theory_of ctxt;
   in
     Output.debug (fn () => "subgoals in isar_atp:\n" ^
                   Pretty.string_of (ProofContext.pretty_term ctxt
@@ -916,22 +917,12 @@
     ResClause.init thy;
     ResHolClause.init thy;
     if !time_limit > 0 then isar_atp (ctxt, goal)
-    else (warning ("Writing problem file only: " ^ !problem_name); 
+    else (warning ("Writing problem file only: " ^ !problem_name);
           isar_atp_writeonly (ctxt, goal))
   end;
 
-val invoke_atp = Toplevel.no_timing o Toplevel.unknown_proof o Toplevel.keep
- (fn state =>
-  let val (ctxt, (_, goal)) = Proof.get_goal (Toplevel.proof_of state)
-  in  invoke_atp_ml (ctxt, goal)  end);
-
-val call_atpP =
-  OuterSyntax.command
-    "ProofGeneral.call_atp"
-    "call automatic theorem provers"
-    OuterKeyword.diag
-    (Scan.succeed invoke_atp);
-
-val _ = OuterSyntax.add_parsers [call_atpP];
+val _ = OuterSyntax.add_parsers
+  [OuterSyntax.command "sledgehammer" "call automatic theorem provers" OuterKeyword.diag
+    (Scan.succeed (Toplevel.no_timing o Toplevel.unknown_proof o Toplevel.keep sledgehammer))];
 
 end;