# HG changeset patch
# User wenzelm
# Date 1376734885 -7200
# Node ID f60f92e472903fa35cd1599108aaa7f9358d7070
# Parent  0f76e620561f3e2fdc6a10c9525cc7c8cd51f610
eliminated pointless subgoal argument;

diff -r 0f76e620561f -r f60f92e47290 src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML	Sat Aug 17 12:13:53 2013 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML	Sat Aug 17 12:21:25 2013 +0200
@@ -500,7 +500,7 @@
     (case try Toplevel.proof_of st of
       SOME state =>
         let
-          val [provers_arg, timeout_arg, subgoal_arg, isar_proofs_arg] = args;
+          val [provers_arg, timeout_arg, isar_proofs_arg] = args;
           val ctxt = Proof.context_of state
           val mode = Normal_Result
 
@@ -515,10 +515,9 @@
             (if provers_arg = "" then [] else [("provers", space_explode " " provers_arg)]))
             |> map (normalize_raw_param ctxt)
 
-          val i = the_default 1 (Int.fromString subgoal_arg)
           val _ =
-            run_sledgehammer (get_params mode ctxt override_params) mode (SOME output_result) i
-              no_fact_override (minimize_command override_params i) state
+            run_sledgehammer (get_params mode ctxt override_params) mode (SOME output_result) 1
+              no_fact_override (minimize_command override_params 1) state
         in () end
     | NONE => error "Unknown proof context"));
 
diff -r 0f76e620561f -r f60f92e47290 src/Tools/jEdit/src/sledgehammer_dockable.scala
--- a/src/Tools/jEdit/src/sledgehammer_dockable.scala	Sat Aug 17 12:13:53 2013 +0200
+++ b/src/Tools/jEdit/src/sledgehammer_dockable.scala	Sat Aug 17 12:21:25 2013 +0200
@@ -106,8 +106,7 @@
   /* controls */
 
   private def clicked {
-    sledgehammer.apply_query(
-      List(provers.getText, timeout.text, subgoal.text, isar_proofs.selected.toString))
+    sledgehammer.apply_query(List(provers.getText, timeout.text, isar_proofs.selected.toString))
   }
 
   private val provers_label = new Label("Provers:") {
@@ -130,12 +129,6 @@
       s match { case Properties.Value.Double(x) => x >= 0.0 case _ => false }
   }
 
-  private val subgoal = new TextField("1", 5) {
-    tooltip = "Subgoal number"
-    verifier = (s: String) =>
-      s match { case Properties.Value.Int(x) => x > 0 case _ => false }
-  }
-
   private val isar_proofs = new CheckBox("Isar proofs") {
     tooltip = "Specify whether Isar proofs should be output in addition to metis line"
     selected = false
@@ -162,7 +155,7 @@
 
   private val controls =
     new FlowPanel(FlowPanel.Alignment.Right)(
-      provers_label, Component.wrap(provers), timeout, subgoal, isar_proofs,
+      provers_label, Component.wrap(provers), timeout, isar_proofs,
       process_indicator.component, apply_query, cancel_query, locate_query, zoom)
   add(controls.peer, BorderLayout.NORTH)
 }