1.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML	Sat Aug 17 12:13:53 2013 +0200
     1.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML	Sat Aug 17 12:21:25 2013 +0200
     1.3 @@ -500,7 +500,7 @@
     1.4      (case try Toplevel.proof_of st of
     1.5        SOME state =>
     1.6          let
     1.7 -          val [provers_arg, timeout_arg, subgoal_arg, isar_proofs_arg] = args;
     1.8 +          val [provers_arg, timeout_arg, isar_proofs_arg] = args;
     1.9            val ctxt = Proof.context_of state
    1.10            val mode = Normal_Result
    1.11  
    1.12 @@ -515,10 +515,9 @@
    1.13              (if provers_arg = "" then [] else [("provers", space_explode " " provers_arg)]))
    1.14              |> map (normalize_raw_param ctxt)
    1.15  
    1.16 -          val i = the_default 1 (Int.fromString subgoal_arg)
    1.17            val _ =
    1.18 -            run_sledgehammer (get_params mode ctxt override_params) mode (SOME output_result) i
    1.19 -              no_fact_override (minimize_command override_params i) state
    1.20 +            run_sledgehammer (get_params mode ctxt override_params) mode (SOME output_result) 1
    1.21 +              no_fact_override (minimize_command override_params 1) state
    1.22          in () end
    1.23      | NONE => error "Unknown proof context"));
    1.24  

     2.1 --- a/src/Tools/jEdit/src/sledgehammer_dockable.scala	Sat Aug 17 12:13:53 2013 +0200
     2.2 +++ b/src/Tools/jEdit/src/sledgehammer_dockable.scala	Sat Aug 17 12:21:25 2013 +0200
     2.3 @@ -106,8 +106,7 @@
     2.4    /* controls */
     2.5  
     2.6    private def clicked {
     2.7 -    sledgehammer.apply_query(
     2.8 -      List(provers.getText, timeout.text, subgoal.text, isar_proofs.selected.toString))
     2.9 +    sledgehammer.apply_query(List(provers.getText, timeout.text, isar_proofs.selected.toString))
    2.10    }
    2.11  
    2.12    private val provers_label = new Label("Provers:") {
    2.13 @@ -130,12 +129,6 @@
    2.14        s match { case Properties.Value.Double(x) => x >= 0.0 case _ => false }
    2.15    }
    2.16  
    2.17 -  private val subgoal = new TextField("1", 5) {
    2.18 -    tooltip = "Subgoal number"
    2.19 -    verifier = (s: String) =>
    2.20 -      s match { case Properties.Value.Int(x) => x > 0 case _ => false }
    2.21 -  }
    2.22 -
    2.23    private val isar_proofs = new CheckBox("Isar proofs") {
    2.24      tooltip = "Specify whether Isar proofs should be output in addition to metis line"
    2.25      selected = false
    2.26 @@ -162,7 +155,7 @@
    2.27  
    2.28    private val controls =
    2.29      new FlowPanel(FlowPanel.Alignment.Right)(
    2.30 -      provers_label, Component.wrap(provers), timeout, subgoal, isar_proofs,
    2.31 +      provers_label, Component.wrap(provers), timeout, isar_proofs,
    2.32        process_indicator.component, apply_query, cancel_query, locate_query, zoom)
    2.33    add(controls.peer, BorderLayout.NORTH)
    2.34  }