src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML

--- a/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML	Tue Apr 27 17:05:39 2010 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML	Tue Apr 27 17:44:33 2010 +0200
@@ -217,20 +217,25 @@
 fun get_params thy = extract_params thy (default_raw_params thy)
 fun default_params thy = get_params thy o map (apsnd single)
 
+val subgoal_count = Logic.count_prems o prop_of o #goal o Proof.goal
+
 (* Sledgehammer the given subgoal *)
 
 fun run {atps = [], ...} _ _ _ _ = error "No ATP is set."
   | run (params as {atps, timeout, ...}) i relevance_override minimize_command
-        proof_state =
-    let
-      val birth_time = Time.now ()
-      val death_time = Time.+ (birth_time, timeout)
-      val _ = kill_atps ()  (* race w.r.t. other invocations of Sledgehammer *)
-      val _ = priority "Sledgehammering..."
-      val _ = List.app (start_prover_thread params birth_time death_time i
-                                            relevance_override minimize_command
-                                            proof_state) atps
-    in () end
+        state =
+    case subgoal_count state of
+      0 => priority "No subgoal!"
+    | n =>
+      let
+        val birth_time = Time.now ()
+        val death_time = Time.+ (birth_time, timeout)
+        val _ = kill_atps ()  (* race w.r.t. other Sledgehammer invocations *)
+        val _ = priority "Sledgehammering..."
+        val _ = app (start_prover_thread params birth_time death_time i n
+                                         relevance_override minimize_command
+                                         state) atps
+      in () end
 
 fun minimize override_params i fact_refs state =
   let
@@ -240,8 +245,10 @@
       map o pairf Facts.string_of_ref o ProofContext.get_fact
     val name_thms_pairs = theorems_from_refs ctxt fact_refs
   in
-    priority (#2 (minimize_theorems (get_params thy override_params) i state
-                                    name_thms_pairs))
+    case subgoal_count state of
+      0 => priority "No subgoal!"
+    | n => priority (#2 (minimize_theorems (get_params thy override_params) i n
+                                           state name_thms_pairs))
   end
 
 val sledgehammerN = "sledgehammer"
@@ -262,9 +269,7 @@
 val is_raw_param_relevant_for_minimize =
   member (op =) params_for_minimize o fst o unalias_raw_param
 fun string_for_raw_param (key, values) =
-  key ^ (case space_implode " " values of
-           "" => ""
-         | value => " = " ^ value)
+  key ^ (case space_implode " " values of "" => "" | value => " = " ^ value)
 
 fun minimize_command override_params i atp_name facts =
   sledgehammerN ^ " " ^ minimizeN ^ " [atp = " ^ atp_name ^
@@ -276,7 +281,7 @@
 fun hammer_away override_params subcommand opt_i relevance_override state =
   let
     val thy = Proof.theory_of state
-    val _ = List.app check_raw_param override_params
+    val _ = app check_raw_param override_params
   in
     if subcommand = runN then
       let val i = the_default 1 opt_i in