diff -r a3793600cb93 -r 4d3527b94f2a src/Pure/Isar/proof.ML
--- a/src/Pure/Isar/proof.ML	Sat Dec 12 15:37:42 2015 +0100
+++ b/src/Pure/Isar/proof.ML	Sun Dec 13 21:56:15 2015 +0100
@@ -35,8 +35,9 @@
   val has_bottom_goal: state -> bool
   val using_facts: thm list -> state -> state
   val pretty_state: state -> Pretty.T list
-  val refine: Method.text -> state -> state Seq.seq
-  val refine_end: Method.text -> state -> state Seq.seq
+  val refine: Method.text -> state -> state Seq.result Seq.seq
+  val refine_end: Method.text -> state -> state Seq.result Seq.seq
+  val refine_singleton: Method.text -> state -> state
   val refine_insert: thm list -> state -> state
   val refine_primitive: (Proof.context -> thm -> thm) -> state -> state
   val raw_goal: state -> {context: context, facts: thm list, goal: thm}
@@ -90,14 +91,11 @@
   val end_block: state -> state
   val begin_notepad: context -> state
   val end_notepad: state -> context
-  val proof: Method.text option -> state -> state Seq.seq
-  val proof_results: Method.text_range option -> state -> state Seq.result Seq.seq
+  val proof: Method.text_range option -> state -> state Seq.result 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_range -> state -> state Seq.result Seq.seq
-  val apply_end_results: Method.text_range -> state -> state Seq.result Seq.seq
+  val apply: Method.text_range -> state -> state Seq.result Seq.seq
+  val apply_end: Method.text_range -> state -> state Seq.result Seq.seq
   val local_qed: Method.text_range option * bool -> state -> state
   val theorem: Method.text option -> (thm list list -> context -> context) ->
     (term * term list) list list -> context -> state
@@ -424,14 +422,13 @@
 
 fun apply_method text ctxt state =
   find_goal state |> (fn (goal_ctxt, {statement, using, goal, before_qed, after_qed}) =>
-    Method.evaluate text ctxt using goal
-    |> Seq.map (fn (meth_cases, goal') =>
+    Method.evaluate text ctxt using (goal_ctxt, goal)
+    |> Seq.map_result (fn (goal_ctxt', goal') =>
       let
-        val goal_ctxt' = goal_ctxt
-          |> Proof_Context.update_cases_legacy (no_goal_cases goal @ goal_cases ctxt goal')
-          |> Proof_Context.update_cases meth_cases;
+        val goal_ctxt'' = goal_ctxt'
+          |> Proof_Context.update_cases_legacy (no_goal_cases goal @ goal_cases ctxt goal');
         val state' = state
-          |> map_goal (K (goal_ctxt', statement, using, goal', before_qed, after_qed));
+          |> map_goal (K (goal_ctxt'', statement, using, goal', before_qed, after_qed));
       in state' end));
 
 in
@@ -439,11 +436,13 @@
 fun refine text state = apply_method text (context_of state) state;
 fun refine_end text state = apply_method text (#1 (find_goal state)) state;
 
-fun refine_insert ths =
-  Seq.hd o refine (Method.Basic (K (Method.insert ths)));
+fun refine_singleton text = refine text #> Seq.the_result "";
 
-fun refine_primitive r =  (* FIXME Seq.Error!? *)
-  Seq.hd o refine (Method.Basic (fn ctxt => fn _ => EMPTY_CASES (PRIMITIVE (r ctxt))));
+fun refine_insert ths =
+  refine_singleton (Method.Basic (K (Method.insert ths)));
+
+fun refine_primitive r =
+  refine_singleton (Method.Basic (fn ctxt => fn _ => Method.CONTEXT_TACTIC (PRIMITIVE (r ctxt))));
 
 end;
 
@@ -924,17 +923,15 @@
 (* sub-proofs *)
 
 fun proof opt_text =
-  assert_backward
-  #> refine (the_default Method.standard_text opt_text)
-  #> Seq.map
-    (using_facts []
-      #> enter_forward
-      #> open_block
-      #> reset_goal);
-
-fun proof_results arg =
-  Seq.APPEND (proof (Method.text arg) #> Seq.make_results,
-    method_error "initial" (Method.position arg));
+  Seq.APPEND
+    (assert_backward
+      #> refine (the_default Method.standard_text (Method.text opt_text))
+      #> Seq.map_result
+        (using_facts []
+          #> enter_forward
+          #> open_block
+          #> reset_goal),
+     method_error "initial" (Method.position opt_text));
 
 fun end_proof bot (prev_pos, (opt_text, immed)) =
   let
@@ -951,8 +948,8 @@
       |> assert_current_goal true
       |> using_facts []
       |> `before_qed |-> (refine o the_default Method.succeed_text)
-      |> Seq.maps (refine finish_text)
-      |> Seq.make_results, method_error "terminal" terminal_pos)
+      |> Seq.maps_results (refine finish_text),
+      method_error "terminal" terminal_pos)
     #> Seq.maps_results (Seq.single o finished_goal finished_pos)
   end;
 
@@ -966,21 +963,18 @@
 
 fun defer i =
   assert_no_chain #>
-  refine (Method.Basic (fn _ => METHOD (fn _ => ASSERT_SUBGOAL defer_tac i))) #> Seq.hd;
+  refine_singleton (Method.Basic (fn _ => METHOD (fn _ => ASSERT_SUBGOAL defer_tac i)));
 
 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;
+  refine_singleton (Method.Basic (fn _ => METHOD (fn _ => ASSERT_SUBGOAL prefer_tac i)));
 
-fun apply_results (text, (pos, _)) =
-  Seq.APPEND (apply text #> Seq.make_results, method_error "" pos);
+fun apply (text, (pos, _)) =
+  Seq.APPEND (assert_backward #> refine text #> Seq.map_result (using_facts []),
+    method_error "" pos);
 
-fun apply_end_results (text, (pos, _)) =
-  Seq.APPEND (apply_end text #> Seq.make_results, method_error "" pos);
+fun apply_end (text, (pos, _)) =
+  Seq.APPEND (assert_forward #> refine_end text, method_error "" pos);
 
 
 
@@ -1002,10 +996,9 @@
   in map (Logic.mk_term o Var) vars end;
 
 fun refine_terms n =
-  refine (Method.Basic (fn ctxt => EMPTY_CASES o
+  refine_singleton (Method.Basic (fn ctxt => Method.CONTEXT_TACTIC o
     K (HEADGOAL (PRECISE_CONJUNCTS n
-      (HEADGOAL (CONJUNCTS (ALLGOALS (resolve_tac ctxt [Drule.termI]))))))))
-  #> Seq.hd;
+      (HEADGOAL (CONJUNCTS (ALLGOALS (resolve_tac ctxt [Drule.termI]))))))));
 
 in
 
@@ -1042,7 +1035,7 @@
     |> chaining ? (`the_facts #-> using_facts)
     |> reset_facts
     |> not (null vars) ? refine_terms (length goal_propss)
-    |> null goal_props ? (refine (Method.Basic Method.assumption) #> Seq.hd)
+    |> null goal_props ? refine_singleton (Method.Basic Method.assumption)
   end;
 
 fun generic_qed state =
@@ -1151,7 +1144,7 @@
 local
 
 fun terminal_proof qeds initial terminal =
-  proof_results (SOME initial) #> Seq.maps_results (qeds (#2 (#2 initial), terminal))
+  proof (SOME initial) #> Seq.maps_results (qeds (#2 (#2 initial), terminal))
   #> Seq.the_result "";
 
 in