clarified defer/prefer: more specific errors;

--- a/src/HOL/BNF/Tools/bnf_tactics.ML	Tue Oct 16 16:50:03 2012 +0200
+++ b/src/HOL/BNF/Tools/bnf_tactics.ML	Tue Oct 16 17:47:23 2012 +0200
@@ -10,7 +10,6 @@
 sig
   val ss_only: thm list -> simpset
 
-  val prefer_tac: int -> tactic
   val select_prem_tac: int -> (int -> tactic) -> int -> int -> tactic
   val fo_rtac: thm -> Proof.context -> int -> tactic
   val unfold_thms_tac: Proof.context -> thm list -> tactic
@@ -39,9 +38,6 @@
 
 fun ss_only thms = Simplifier.clear_ss HOL_basic_ss addsimps thms;
 
-(* FIXME: why not in "Pure"? *)
-fun prefer_tac i = defer_tac i THEN PRIMITIVE (Thm.permute_prems 0 ~1);
-
 fun select_prem_tac n tac k = DETERM o (EVERY' [REPEAT_DETERM_N (k - 1) o etac thin_rl,
   tac, REPEAT_DETERM_N (n - k) o etac thin_rl]);
 

--- a/src/Pure/Isar/isar_syn.ML	Tue Oct 16 16:50:03 2012 +0200
+++ b/src/Pure/Isar/isar_syn.ML	Tue Oct 16 17:47:23 2012 +0200
@@ -681,12 +681,11 @@
 
 val _ =
   Outer_Syntax.command @{command_spec "defer"} "shuffle internal proof state"
-    (Scan.option Parse.nat >> (fn n =>
-      (Toplevel.print o Toplevel.proofs (Seq.make_results o Proof.defer n))));
+    (Scan.optional Parse.nat 1 >> (fn n => Toplevel.print o Toplevel.proof (Proof.defer n)));
 
 val _ =
   Outer_Syntax.command @{command_spec "prefer"} "shuffle internal proof state"
-    (Parse.nat >> (fn n => Toplevel.print o Toplevel.proofs (Seq.make_results o Proof.prefer n)));
+    (Parse.nat >> (fn n => Toplevel.print o Toplevel.proof (Proof.prefer n)));
 
 val _ =
   Outer_Syntax.command @{command_spec "apply"} "initial refinement step (unstructured)"

--- a/src/Pure/Isar/method.ML	Tue Oct 16 16:50:03 2012 +0200
+++ b/src/Pure/Isar/method.ML	Tue Oct 16 17:47:23 2012 +0200
@@ -20,8 +20,6 @@
   val SIMPLE_METHOD: tactic -> method
   val SIMPLE_METHOD': (int -> tactic) -> method
   val SIMPLE_METHOD'': ((int -> tactic) -> tactic) -> (int -> tactic) -> method
-  val defer: int option -> method
-  val prefer: int -> method
   val cheating: bool -> Proof.context -> method
   val intro: thm list -> method
   val elim: thm list -> method
@@ -124,12 +122,6 @@
 end;
 
 
-(* shuffle subgoals *)
-
-fun prefer i = METHOD (K (Tactic.defer_tac i THEN PRIMITIVE (Thm.permute_prems 0 ~1)));
-fun defer opt_i = METHOD (K (Tactic.defer_tac (the_default 1 opt_i)));
-
-
 (* cheating *)
 
 fun cheating int ctxt =

--- a/src/Pure/Isar/proof.ML	Tue Oct 16 16:50:03 2012 +0200
+++ b/src/Pure/Isar/proof.ML	Tue Oct 16 17:47:23 2012 +0200
@@ -78,8 +78,8 @@
   val end_notepad: state -> context
   val proof: Method.text option -> state -> state Seq.seq
   val proof_results: Method.text option -> state -> state Seq.result Seq.seq
-  val defer: int option -> state -> state Seq.seq
-  val prefer: int -> state -> state Seq.seq
+  val defer: int -> state -> state
+  val prefer: int -> state -> state
   val apply: Method.text -> state -> state Seq.seq
   val apply_end: Method.text -> state -> state Seq.seq
   val apply_results: Method.text -> state -> state Seq.result Seq.seq
@@ -835,8 +835,13 @@
 
 (* unstructured refinement *)
 
-fun defer i = assert_no_chain #> refine (Method.Basic (K (Method.defer i)));
-fun prefer i = assert_no_chain #> refine (Method.Basic (K (Method.prefer i)));
+fun defer i =
+  assert_no_chain #>
+  refine (Method.Basic (fn _ => METHOD (fn _ => ASSERT_SUBGOAL defer_tac i))) #> Seq.hd;
+
+fun prefer i =
+  assert_no_chain #>
+  refine (Method.Basic (fn _ => METHOD (fn _ => ASSERT_SUBGOAL prefer_tac i))) #> Seq.hd;
 
 fun apply text = assert_backward #> refine text #> Seq.map (using_facts []);
 fun apply_end text = assert_forward #> refine_end text;

--- a/src/Pure/logic.ML	Tue Oct 16 16:50:03 2012 +0200
+++ b/src/Pure/logic.ML	Tue Oct 16 17:47:23 2012 +0200
@@ -557,8 +557,10 @@
 
 (* goal states *)
 
-fun get_goal st i = nth_prem (i, st)
-  handle TERM _ => error "Goal number out of range";
+fun get_goal st i =
+  nth_prem (i, st) handle TERM _ =>
+    error ("Subgoal number " ^ string_of_int i ^ " out of range (a total of " ^
+      string_of_int (count_prems st)  ^ " subgoals)");
 
 (*reverses parameters for substitution*)
 fun goal_params st i =

--- a/src/Pure/tactic.ML	Tue Oct 16 16:50:03 2012 +0200
+++ b/src/Pure/tactic.ML	Tue Oct 16 17:47:23 2012 +0200
@@ -53,6 +53,7 @@
   val rename_tac: string list -> int -> tactic
   val rotate_tac: int -> int -> tactic
   val defer_tac: int -> tactic
+  val prefer_tac: int -> tactic
   val filter_prems_tac: (term -> bool) -> int -> tactic
 end;
 
@@ -318,6 +319,9 @@
 (*Rotates the given subgoal to be the last.*)
 fun defer_tac i = PRIMITIVE (Thm.permute_prems (i - 1) 1);
 
+(*Rotates the given subgoal to be the first.*)
+fun prefer_tac i = PRIMITIVE (Thm.permute_prems (i - 1) 1 #> Thm.permute_prems 0 ~1);
+
 (* remove premises that do not satisfy p; fails if all prems satisfy p *)
 fun filter_prems_tac p =
   let fun Then NONE tac = SOME tac

--- a/src/Pure/tactical.ML	Tue Oct 16 16:50:03 2012 +0200
+++ b/src/Pure/tactical.ML	Tue Oct 16 17:47:23 2012 +0200
@@ -55,6 +55,7 @@
   val TRYALL: (int -> tactic) -> tactic
   val CSUBGOAL: ((cterm * int) -> tactic) -> int -> tactic
   val SUBGOAL: ((term * int) -> tactic) -> int -> tactic
+  val ASSERT_SUBGOAL: (int -> tactic) -> int -> tactic
   val CHANGED_GOAL: (int -> tactic) -> int -> tactic
   val SOLVED': (int -> tactic) -> int -> tactic
   val THEN_ALL_NEW: (int -> tactic) * (int -> tactic) -> int -> tactic
@@ -328,6 +329,8 @@
 fun SUBGOAL goalfun =
   CSUBGOAL (fn (goal, i) => goalfun (Thm.term_of goal, i));
 
+fun ASSERT_SUBGOAL (tac: int -> tactic) i st = (Logic.get_goal (Thm.prop_of st) i; tac i st);
+
 (*Returns all states that have changed in subgoal i, counted from the LAST
   subgoal.  For stac, for example.*)
 fun CHANGED_GOAL tac i st =