qed/after_qed: singleton result;

--- a/src/Pure/Isar/expression.ML	Wed Jan 07 12:10:22 2009 +0100
+++ b/src/Pure/Isar/expression.ML	Wed Jan 07 16:22:10 2009 +0100
@@ -887,7 +887,7 @@
       end;
 
     fun after_qed results =
-      Proof.map_context (fold store_reg (regs ~~ prep_result propss results)) #> Seq.single;
+      Proof.map_context (fold store_reg (regs ~~ prep_result propss results));
   in
     state |> Proof.map_context (K goal_ctxt) |>
       Proof.local_goal (ProofDisplay.print_results int) (K I) ProofContext.bind_propp_i

--- a/src/Pure/Isar/isar_cmd.ML	Wed Jan 07 12:10:22 2009 +0100
+++ b/src/Pure/Isar/isar_cmd.ML	Wed Jan 07 16:22:10 2009 +0100
@@ -1,5 +1,4 @@
 (*  Title:      Pure/Isar/isar_cmd.ML
-    ID:         $Id$
     Author:     Markus Wenzel, TU Muenchen
 
 Derived Isar commands.
@@ -219,7 +218,7 @@
 (* goals *)
 
 fun goal opt_chain goal stmt int =
-  opt_chain #> goal NONE (K Seq.single) stmt int;
+  opt_chain #> goal NONE (K I) stmt int;
 
 val have = goal I Proof.have;
 val hence = goal Proof.chain Proof.have;
@@ -229,12 +228,12 @@
 
 (* local endings *)
 
-fun local_qed m = Toplevel.proofs (Proof.local_qed (m, true));
-val local_terminal_proof = Toplevel.proofs o Proof.local_terminal_proof;
-val local_default_proof = Toplevel.proofs Proof.local_default_proof;
-val local_immediate_proof = Toplevel.proofs Proof.local_immediate_proof;
-val local_done_proof = Toplevel.proofs Proof.local_done_proof;
-val local_skip_proof = Toplevel.proofs' Proof.local_skip_proof;
+fun local_qed m = Toplevel.proof (Proof.local_qed (m, true));
+val local_terminal_proof = Toplevel.proof o Proof.local_terminal_proof;
+val local_default_proof = Toplevel.proof Proof.local_default_proof;
+val local_immediate_proof = Toplevel.proof Proof.local_immediate_proof;
+val local_done_proof = Toplevel.proof Proof.local_done_proof;
+val local_skip_proof = Toplevel.proof' Proof.local_skip_proof;
 
 val skip_local_qed = Toplevel.skip_proof (fn i => if i > 1 then i - 1 else raise Toplevel.UNDEF);
 

--- a/src/Pure/Isar/obtain.ML	Wed Jan 07 12:10:22 2009 +0100
+++ b/src/Pure/Isar/obtain.ML	Wed Jan 07 16:22:10 2009 +0100
@@ -1,5 +1,4 @@
 (*  Title:      Pure/Isar/obtain.ML
-    ID:         $Id$
     Author:     Markus Wenzel, TU Muenchen
 
 The 'obtain' and 'guess' language elements -- generalized existence at
@@ -150,13 +149,13 @@
 
     fun after_qed _ =
       Proof.local_qed (NONE, false)
-      #> Seq.map (`Proof.the_fact #-> (fn rule =>
+      #> `Proof.the_fact #-> (fn rule =>
         Proof.fix_i vars
-        #> Proof.assm_i (obtain_export fix_ctxt rule (map (cert o Free) parms)) asms));
+        #> Proof.assm_i (obtain_export fix_ctxt rule (map (cert o Free) parms)) asms);
   in
     state
     |> Proof.enter_forward
-    |> Proof.have_i NONE (K Seq.single) [((Binding.empty, []), [(obtain_prop, [])])] int
+    |> Proof.have_i NONE (K I) [((Binding.empty, []), [(obtain_prop, [])])] int
     |> Proof.proof (SOME Method.succeed_text) |> Seq.hd
     |> Proof.fix_i [(Binding.name thesisN, NONE, NoSyn)]
     |> Proof.assume_i
@@ -306,7 +305,7 @@
     val before_qed = SOME (Method.primitive_text (Goal.conclude #> MetaSimplifier.norm_hhf #>
         (fn th => Goal.protect (Conjunction.intr (Drule.mk_term (Thm.cprop_of th)) th))));
     fun after_qed [[_, res]] =
-      Proof.end_block #> guess_context (check_result ctxt thesis res) #> Seq.single;
+      Proof.end_block #> guess_context (check_result ctxt thesis res);
   in
     state
     |> Proof.enter_forward

--- a/src/Pure/Isar/old_locale.ML	Wed Jan 07 12:10:22 2009 +0100
+++ b/src/Pure/Isar/old_locale.ML	Wed Jan 07 16:22:10 2009 +0100
@@ -116,7 +116,7 @@
     theory -> Proof.state
   val interpretation_in_locale: (Proof.context -> Proof.context) ->
     xstring * expr -> theory -> Proof.state
-  val interpret: (Proof.state -> Proof.state Seq.seq) ->
+  val interpret: (Proof.state -> Proof.state) ->
     (Binding.T -> Binding.T) -> expr ->
     term option list * (Attrib.binding * term) list ->
     bool -> Proof.state ->
@@ -2478,7 +2478,7 @@
 
 val interpret = gen_interpret prep_local_registration;
 fun interpret_cmd interp_prfx = snd oooo gen_interpret prep_local_registration_cmd
-  Seq.single (standard_name_morph interp_prfx);
+  I (standard_name_morph interp_prfx);
 
 end;
 

--- a/src/Pure/Isar/proof.ML	Wed Jan 07 12:10:22 2009 +0100
+++ b/src/Pure/Isar/proof.ML	Wed Jan 07 16:22:10 2009 +0100
@@ -87,31 +87,31 @@
   val local_goal: (context -> ((string * string) * (string * thm list) list) -> unit) ->
     (theory -> 'a -> attribute) ->
     (context * 'b list -> context * (term list list * (context -> context))) ->
-    string -> Method.text option -> (thm list list -> state -> state Seq.seq) ->
+    string -> Method.text option -> (thm list list -> state -> state) ->
     ((Binding.T * 'a list) * 'b) list -> state -> state
-  val local_qed: Method.text option * bool -> state -> state Seq.seq
+  val local_qed: Method.text option * bool -> state -> state
   val theorem: Method.text option -> (thm list list -> context -> context) ->
     (string * string list) list list -> context -> state
   val theorem_i: Method.text option -> (thm list list -> context -> context) ->
     (term * term list) list list -> context -> state
   val global_qed: Method.text option * bool -> state -> context
-  val local_terminal_proof: Method.text * Method.text option -> state -> state Seq.seq
-  val local_default_proof: state -> state Seq.seq
-  val local_immediate_proof: state -> state Seq.seq
-  val local_done_proof: state -> state Seq.seq
-  val local_skip_proof: bool -> state -> state Seq.seq
+  val local_terminal_proof: Method.text * Method.text option -> state -> state
+  val local_default_proof: state -> state
+  val local_immediate_proof: state -> state
+  val local_skip_proof: bool -> state -> state
+  val local_done_proof: state -> state
   val global_terminal_proof: Method.text * Method.text option -> state -> context
   val global_default_proof: state -> context
   val global_immediate_proof: state -> context
+  val global_skip_proof: bool -> state -> context
   val global_done_proof: state -> context
-  val global_skip_proof: bool -> state -> context
-  val have: Method.text option -> (thm list list -> state -> state Seq.seq) ->
+  val have: Method.text option -> (thm list list -> state -> state) ->
     (Attrib.binding * (string * string list) list) list -> bool -> state -> state
-  val have_i: Method.text option -> (thm list list -> state -> state Seq.seq) ->
+  val have_i: Method.text option -> (thm list list -> state -> state) ->
     ((Binding.T * attribute list) * (term * term list) list) list -> bool -> state -> state
-  val show: Method.text option -> (thm list list -> state -> state Seq.seq) ->
+  val show: Method.text option -> (thm list list -> state -> state) ->
     (Attrib.binding * (string * string list) list) list -> bool -> state -> state
-  val show_i: Method.text option -> (thm list list -> state -> state Seq.seq) ->
+  val show_i: Method.text option -> (thm list list -> state -> state) ->
     ((Binding.T * attribute list) * (term * term list) list) list -> bool -> state -> state
   val is_relevant: state -> bool
   val future_proof: (state -> ('a * context) future) -> state -> 'a future * context
@@ -148,7 +148,7 @@
     goal: thm,                            (*subgoals ==> statement*)
     before_qed: Method.text option,
     after_qed:
-      (thm list list -> state -> state Seq.seq) *
+      (thm list list -> state -> state) *
       (thm list list -> context -> context)};
 
 fun make_goal (statement, messages, using, goal, before_qed, after_qed) =
@@ -347,8 +347,7 @@
       (case filter_out (fn s => s = "") strs of [] => ""
       | strs' => enclose " (" ")" (commas strs'));
 
-    fun prt_goal (SOME (ctxt, (i,
-            {statement = ((_, pos), _, _), messages, using, goal, before_qed, after_qed}))) =
+    fun prt_goal (SOME (ctxt, (i, {statement = ((_, pos), _, _), messages, using, goal, ...}))) =
           pretty_facts "using " ctxt
             (if mode <> Backward orelse null using then NONE else SOME using) @
           [Pretty.str ("goal" ^
@@ -751,6 +750,13 @@
   |> `before_qed |-> (refine o the_default Method.succeed_text)
   |> Seq.maps (refine (Method.finish_text txt (Position.thread_data ())));
 
+fun check_result msg sq =
+  (case Seq.pull sq of
+    NONE => error msg
+  | SOME (s, _) => s);
+
+fun check_finish sq = check_result "Failed to finish proof" sq;
+
 
 (* unstructured refinement *)
 
@@ -842,7 +848,7 @@
       |> burrow (ProofContext.export goal_ctxt outer_ctxt);
 
     val (after_local, after_global) = after_qed;
-    fun after_local' x y = Position.setmp_thread_data_seq pos (fn () => after_local x y) ();
+    fun after_local' x y = Position.setmp_thread_data pos (fn () => after_local x y) ();
     fun after_global' x y = Position.setmp_thread_data pos (fn () => after_global x y) ();
   in
     outer_state
@@ -871,61 +877,47 @@
     |> tap (Variable.warn_extra_tfrees (context_of state) o context_of)
   end;
 
-fun local_qed txt =
-  end_proof false txt #>
-  Seq.maps (generic_qed ProofContext.auto_bind_facts #->
+fun local_qeds txt =
+  end_proof false txt
+  #> Seq.map (generic_qed ProofContext.auto_bind_facts #->
     (fn ((after_qed, _), results) => after_qed results));
 
+fun local_qed txt = local_qeds txt #> check_finish;
+
 
 (* global goals *)
 
 fun global_goal prepp before_qed after_qed propp ctxt =
   init ctxt
-  |> generic_goal (prepp #> ProofContext.auto_fixes) ""
-    before_qed (K Seq.single, after_qed) propp;
+  |> generic_goal (prepp #> ProofContext.auto_fixes) "" before_qed (K I, after_qed) propp;
 
 val theorem = global_goal ProofContext.bind_propp_schematic;
 val theorem_i = global_goal ProofContext.bind_propp_schematic_i;
 
-fun check_result msg sq =
-  (case Seq.pull sq of
-    NONE => error msg
-  | SOME (s', sq') => Seq.cons s' sq');
-
 fun global_qeds txt =
   end_proof true txt
   #> Seq.map (generic_qed (K I) #> (fn (((_, after_qed), results), state) =>
-    after_qed results (context_of state)))
-  |> Seq.DETERM;   (*backtracking may destroy theory!*)
+    after_qed results (context_of state)));
 
-fun global_qed txt =
-  global_qeds txt
-  #> check_result "Failed to finish proof"
-  #> Seq.hd;
+fun global_qed txt = global_qeds txt #> check_finish;
 
 
 (* concluding steps *)
 
-fun local_terminal_proof (text, opt_text) =
-  proof (SOME text) #> Seq.maps (local_qed (opt_text, true));
+fun terminal_proof qed initial terminal =
+  proof (SOME initial) #> Seq.maps (qed terminal) #> check_finish;
 
+fun local_terminal_proof (text, opt_text) = terminal_proof local_qeds text (opt_text, true);
 val local_default_proof = local_terminal_proof (Method.default_text, NONE);
 val local_immediate_proof = local_terminal_proof (Method.this_text, NONE);
-val local_done_proof = proof (SOME Method.done_text) #> Seq.maps (local_qed (NONE, false));
 fun local_skip_proof int = local_terminal_proof (Method.sorry_text int, NONE);
+val local_done_proof = terminal_proof local_qeds Method.done_text (NONE, false);
 
-fun global_term_proof immed (text, opt_text) =
-  proof (SOME text)
-  #> check_result "Terminal proof method failed"
-  #> Seq.maps (global_qeds (opt_text, immed))
-  #> check_result "Failed to finish proof (after successful terminal method)"
-  #> Seq.hd;
-
-val global_terminal_proof = global_term_proof true;
+fun global_terminal_proof (text, opt_text) = terminal_proof global_qeds text (opt_text, true);
 val global_default_proof = global_terminal_proof (Method.default_text, NONE);
 val global_immediate_proof = global_terminal_proof (Method.this_text, NONE);
-val global_done_proof = global_term_proof false (Method.done_text, NONE);
 fun global_skip_proof int = global_terminal_proof (Method.sorry_text int, NONE);
+val global_done_proof = terminal_proof global_qeds Method.done_text (NONE, false);
 
 
 (* common goal statements *)
@@ -940,7 +932,7 @@
     val testing = ref false;
     val rule = ref (NONE: thm option);
     fun fail_msg ctxt =
-      "Local statement will fail to solve any pending goal" ::
+      "Local statement will fail to refine any pending goal" ::
       (case ! rule of NONE => [] | SOME th => [ProofDisplay.string_of_rule ctxt "Failed" th])
       |> cat_lines;
 
@@ -951,13 +943,14 @@
       else if int then priority (ProofDisplay.string_of_rule ctxt "Successful" th)
       else ();
     val test_proof =
-      (Seq.pull oo local_skip_proof) true
+      try (local_skip_proof true)
       |> setmp_noncritical testing true
       |> Exn.capture;
 
     fun after_qed' results =
       refine_goals print_rule (context_of state) (flat results)
-      #> Seq.maps (after_qed results);
+      #> check_result "Failed to refine any pending goal"
+      #> after_qed results;
   in
     state
     |> local_goal print_results prep_att prepp "show" before_qed after_qed' stmt
@@ -998,12 +991,12 @@
 
 fun future_proof fork_proof state =
   let
-    val _ = is_relevant state andalso error "Cannot fork relevant proof";
-
     val _ = assert_backward state;
     val (goal_ctxt, (_, goal)) = find_goal state;
     val {statement as (kind, propss, prop), messages, using, goal, before_qed, after_qed} = goal;
 
+    val _ = is_relevant state andalso error "Cannot fork relevant proof";
+
     val prop' = Logic.protect prop;
     val statement' = (kind, [[], [prop']], prop');
     val goal' = Thm.adjust_maxidx_thm (Thm.maxidx_of goal)

--- a/src/Pure/Tools/invoke.ML	Wed Jan 07 12:10:22 2009 +0100
+++ b/src/Pure/Tools/invoke.ML	Wed Jan 07 16:22:10 2009 +0100
@@ -88,7 +88,7 @@
           |> (snd o ProofContext.note_thmss_i "" notes)
           |> ProofContext.restore_naming ctxt
         end) #>
-      Proof.put_facts NONE #> Seq.single;
+      Proof.put_facts NONE;
   in
     state'
     |> Proof.chain_facts chain_facts