After_qed takes result argument.

--- a/src/Pure/Isar/isar_thy.ML	Mon Aug 08 22:11:31 2005 +0200
+++ b/src/Pure/Isar/isar_thy.ML	Mon Aug 08 22:14:04 2005 +0200
@@ -58,24 +58,31 @@
     -> bool -> theory -> ProofHistory.T
   val theorem_i: string -> (bstring * theory attribute list) *
     (term * (term list * term list)) -> bool -> theory -> ProofHistory.T
-  val multi_theorem: string -> (theory -> theory) ->
+  val multi_theorem: string -> (thm list * thm list -> theory -> theory) ->
     (cterm list -> Proof.context -> Proof.context -> thm -> thm) ->
     bstring * Attrib.src list -> Locale.element Locale.elem_expr list ->
     ((bstring * Attrib.src list) * (string * (string list * string list)) list) list
     -> bool -> theory -> ProofHistory.T
-  val multi_theorem_i: string -> (theory -> theory) ->
+  val multi_theorem_i: string -> (thm list * thm list -> theory -> theory) ->
+    (cterm list -> Proof.context -> Proof.context -> thm -> thm) ->
+    bstring * theory attribute list ->
+    Locale.element_i Locale.elem_expr list ->
+    ((bstring * theory attribute list) * (term * (term list * term list)) list) list ->
+    bool -> theory -> ProofHistory.T
+  val locale_multi_theorem:
+    string -> (thm list * thm list -> theory -> theory) ->
     (cterm list -> Proof.context -> Proof.context -> thm -> thm) ->
-    bstring * theory attribute list -> Locale.element_i Locale.elem_expr list
-    -> ((bstring * theory attribute list) * (term * (term list * term list)) list) list
-    -> bool -> theory -> ProofHistory.T
-  val locale_multi_theorem: string -> xstring
-    -> bstring * Attrib.src list -> Locale.element Locale.elem_expr list
-    -> ((bstring * Attrib.src list) * (string * (string list * string list)) list) list
-    -> bool -> theory -> ProofHistory.T
-  val locale_multi_theorem_i: string -> string -> bstring * Attrib.src list
-    -> Locale.element_i Locale.elem_expr list
-    -> ((bstring * Attrib.src list) * (term * (term list * term list)) list) list
-    -> bool -> theory -> ProofHistory.T
+    xstring ->
+    bstring * Attrib.src list -> Locale.element Locale.elem_expr list ->
+    ((bstring * Attrib.src list) * (string * (string list * string list)) list) list ->
+    bool -> theory -> ProofHistory.T
+  val locale_multi_theorem_i:
+    string -> (thm list * thm list -> theory -> theory) ->
+    (cterm list -> Proof.context -> Proof.context -> thm -> thm) ->
+    string ->
+    bstring * Attrib.src list -> Locale.element_i Locale.elem_expr list ->
+    ((bstring * Attrib.src list) * (term * (term list * term list)) list) list ->
+    bool -> theory -> ProofHistory.T
   val smart_multi_theorem: string -> xstring option
     -> bstring * Attrib.src list -> Locale.element Locale.elem_expr list
     -> ((bstring * Attrib.src list) * (string * (string list * string list)) list) list
@@ -386,8 +393,8 @@
 fun multi_theorem_i k after_qed export a =
   global_statement_i o Proof.multi_theorem_i k after_qed export NONE a;
 
-fun locale_multi_theorem k locale (name, atts) elems concl int thy =
-  global_statement (Proof.multi_theorem k I  ProofContext.export_standard
+fun locale_multi_theorem k after_qed export locale (name, atts) elems concl int thy =
+  global_statement (Proof.multi_theorem k after_qed export
       (SOME (locale,
         (map (Attrib.intern_src thy) atts,
          map (map (Attrib.intern_src thy) o snd o fst) concl)))
@@ -395,34 +402,34 @@
       (map (Locale.intern_attrib_elem_expr thy) elems))
     (map (apfst (apsnd (K []))) concl) int thy;
 
-fun locale_multi_theorem_i k locale (name, atts) elems concl =
-  global_statement_i (Proof.multi_theorem_i k I ProofContext.export_standard
+fun locale_multi_theorem_i k after_qed export locale (name, atts) elems concl =
+  global_statement_i (Proof.multi_theorem_i k after_qed export
       (SOME (locale, (atts, map (snd o fst) concl)))
       (name, []) elems) (map (apfst (apsnd (K []))) concl);
 
 fun theorem k (a, t) =
-  multi_theorem k I ProofContext.export_standard a [] [(("", []), [t])];
+  multi_theorem k (K I) ProofContext.export_standard a [] [(("", []), [t])];
 
 fun theorem_i k (a, t) =
-  multi_theorem_i k I ProofContext.export_standard a [] [(("", []), [t])];
+  multi_theorem_i k (K I) ProofContext.export_standard a [] [(("", []), [t])];
 
 fun smart_multi_theorem k NONE a elems =
-      multi_theorem k I ProofContext.export_standard a elems
+      multi_theorem k (K I) ProofContext.export_standard a elems
   | smart_multi_theorem k (SOME locale) a elems =
-      locale_multi_theorem k locale a elems;
+      locale_multi_theorem k (K I) ProofContext.export_standard locale a elems;
 
 val assume      = local_statement Proof.assume I;
 val assume_i    = local_statement_i Proof.assume_i I;
 val presume     = local_statement Proof.presume I;
 val presume_i   = local_statement_i Proof.presume_i I;
-val have        = local_statement (Proof.have Seq.single true) I;
-val have_i      = local_statement_i (Proof.have_i Seq.single true) I;
-val hence       = local_statement (Proof.have Seq.single true) Proof.chain;
-val hence_i     = local_statement_i (Proof.have_i Seq.single true) Proof.chain;
-val show        = local_statement' (Proof.show check_goal Seq.single true) I;
-val show_i      = local_statement_i' (Proof.show_i check_goal Seq.single true) I;
-val thus        = local_statement' (Proof.show check_goal Seq.single true) Proof.chain;
-val thus_i      = local_statement_i' (Proof.show_i check_goal Seq.single true) Proof.chain;
+val have        = local_statement (Proof.have (K Seq.single) true) I;
+val have_i      = local_statement_i (Proof.have_i (K Seq.single) true) I;
+val hence       = local_statement (Proof.have (K Seq.single) true) Proof.chain;
+val hence_i     = local_statement_i (Proof.have_i (K Seq.single) true) Proof.chain;
+val show        = local_statement' (Proof.show check_goal (K Seq.single) true) I;
+val show_i      = local_statement_i' (Proof.show_i check_goal (K Seq.single) true) I;
+val thus        = local_statement' (Proof.show check_goal (K Seq.single) true) Proof.chain;
+val thus_i      = local_statement_i' (Proof.show_i check_goal (K Seq.single) true) Proof.chain;
 
 fun gen_def f ((name, srcs), def) = ProofHistory.apply (fn state =>
   f name (map (Attrib.local_attribute (Proof.theory_of state)) srcs) def state);
@@ -641,59 +648,42 @@
 
 fun register_globally (((prfx, atts), expr), insts) int thy =
   let
-    val (thy', propss, activate) =
+    val (propss, after_qed) =
       Locale.prep_global_registration (prfx, atts) expr insts thy;
-    fun witness id (thy, thm) = let
-        val thm' = Drule.freeze_all thm;
-      in
-        (Locale.add_global_witness id thm' thy, thm')
-      end;
   in
-    multi_theorem_i Drule.internalK activate ProofContext.export_plain
+    multi_theorem_i Drule.internalK (fst #> after_qed) ProofContext.export_plain
       ("", []) []
-      (map (fn ((n, ps), props) =>
-          ((NameSpace.base n, [witness (n, map Logic.varify ps)]),
-        map (fn prop => (prop, ([], []))) props)) propss) int thy'
-  end;
-
-fun register_in_locale (target, expr) int thy =
-  let
-    val target = Locale.intern thy target;
-    val (target_expr, thy', propss, activate) =
-        Locale.prep_registration_in_locale target expr thy;
-    fun witness id (thy, thm) = let
-        (* push outer quantifiers inside implications *)
-        val {prop, sign, ...} = rep_thm thm;
-        val frees = map (cterm_of sign o Free) (strip_all_vars prop);
-            (* are hopefully distinct *)
-        val prems = Logic.strip_imp_prems (strip_all_body prop);
-        val cprems = map (cterm_of sign) prems;
-        val thm' = thm |> forall_elim_list frees
-                       |> (fn th => implies_elim_list th (map Thm.assume cprems))
-                       |> forall_intr_list frees;
-      in (Locale.add_witness_in_locale target id thm' thy, thm') end;
-  in
-    multi_theorem_i Drule.internalK activate ProofContext.export_plain
-      ("",[]) [Locale.Expr target_expr]
-      (map (fn (id as (n, _), props) => ((NameSpace.base n, [witness id]),
-        map (fn prop => (prop, ([], []))) props)) propss) int thy'
+      (map (fn ((n, _), props) => ((NameSpace.base n, []),
+        map (fn prop => (prop, ([], []))) props)) propss) int thy
   end;
 
 fun register_locally (((prfx, atts), expr), insts) =
   ProofHistory.apply (fn state =>
     let
       val ctxt = Proof.context_of state;
-      val (ctxt', propss, activate) =
+      val (propss, after_qed) =
         Locale.prep_local_registration (prfx, atts) expr insts ctxt;
-      fun witness id (ctxt, thm) = (Locale.add_local_witness id thm ctxt, thm);
     in
       state
-      |> Proof.map_context (fn _ => ctxt')
-      |> Proof.have_i (Seq.single o Proof.map_context activate) true
-        (map (fn (id as (n, _), props) => ((NameSpace.base n, [witness id]),
+      |> Proof.map_context (fn _ => ctxt)
+      |> Proof.have_i (fn result => Seq.single o Proof.map_context (after_qed result)) true
+        (map (fn ((n, _), props) => ((NameSpace.base n, []),
           map (fn prop => (prop, ([], []))) props)) propss)
     end);
 
+fun register_in_locale (target, expr) int thy =
+  let
+    val target = Locale.intern thy target;
+    val (propss, after_qed) =
+        Locale.prep_registration_in_locale target expr thy;
+  in
+    locale_multi_theorem_i Drule.internalK (fst #> after_qed)
+      ProofContext.export_plain
+      target ("",[]) []
+      (map (fn ((n, _), props) => ((NameSpace.base n, []),
+        map (fn prop => (prop, ([], []))) props)) propss) int thy
+  end;
+
 
 (* theory init and exit *)
 

--- a/src/Pure/Isar/obtain.ML	Mon Aug 08 22:11:31 2005 +0200
+++ b/src/Pure/Isar/obtain.ML	Mon Aug 08 22:14:04 2005 +0200
@@ -106,7 +106,7 @@
       Logic.list_rename_params ([AutoBind.thesisN],
         Term.list_all_free ([bound_thesis_var], Logic.mk_implies (that_prop, bound_thesis)));
 
-    fun after_qed st = st
+    fun after_qed _ st = st
       |> Method.local_qed false NONE print
       |> Seq.map (fn st' => st'
         |> Proof.fix_i vars
@@ -114,7 +114,7 @@
   in
     state
     |> Proof.enter_forward
-    |> Proof.have_i Seq.single true [(("", []), [(obtain_prop, ([], []))])]
+    |> Proof.have_i (K Seq.single) true [(("", []), [(obtain_prop, ([], []))])]
     |> Method.proof (SOME (Method.Basic (K Method.succeed))) |> Seq.hd
     |> Proof.fix_i [([thesisN], NONE)]
     |> Proof.assume_i [((thatN, [ContextRules.intro_query_local NONE]), [(that_prop, ([], []))])]

--- a/src/Pure/Isar/proof.ML	Mon Aug 08 22:11:31 2005 +0200
+++ b/src/Pure/Isar/proof.ML	Mon Aug 08 22:14:04 2005 +0200
@@ -85,13 +85,13 @@
   val def: string -> context attribute list -> string *  (string * string list) -> state -> state
   val def_i: string -> context attribute list -> string * (term * term list) -> state -> state
   val invoke_case: string * string option list * context attribute list -> state -> state
-  val multi_theorem: string -> (theory -> theory) ->
+  val multi_theorem: string -> (thm list * thm list -> theory -> theory) ->
     (cterm list -> context -> context -> thm -> thm) ->
     (xstring * (Attrib.src list * Attrib.src list list)) option ->
     bstring * theory attribute list -> Locale.element Locale.elem_expr list
     -> ((bstring * theory attribute list) * (string * (string list * string list)) list) list
     -> theory -> state
-  val multi_theorem_i: string -> (theory -> theory) ->
+  val multi_theorem_i: string -> (thm list * thm list -> theory -> theory) ->
     (cterm list -> context -> context -> thm -> thm) ->
     (string * (Attrib.src list * Attrib.src list list)) option
     -> bstring * theory attribute list
@@ -100,16 +100,16 @@
     -> theory -> state
   val chain: state -> state
   val from_facts: thm list -> state -> state
-  val show: (bool -> state -> state) -> (state -> state Seq.seq) -> bool
+  val show: (bool -> state -> state) -> (thm list -> state -> state Seq.seq) -> bool
     -> ((string * context attribute list) * (string * (string list * string list)) list) list
     -> bool -> state -> state
-  val show_i: (bool -> state -> state) -> (state -> state Seq.seq) -> bool
+  val show_i: (bool -> state -> state) -> (thm list -> state -> state Seq.seq) -> bool
     -> ((string * context attribute list) * (term * (term list * term list)) list) list
     -> bool -> state -> state
-  val have: (state -> state Seq.seq) -> bool
+  val have: (thm list -> state -> state Seq.seq) -> bool
     -> ((string * context attribute list) * (string * (string list * string list)) list) list
     -> state -> state
-  val have_i: (state -> state Seq.seq) -> bool
+  val have_i: (thm list -> state -> state Seq.seq) -> bool
     -> ((string * context attribute list) * (term * (term list * term list)) list) list
     -> state -> state
   val at_bottom: state -> bool
@@ -178,7 +178,9 @@
     node *              (*current*)
     node list           (*parents wrt. block structure*)
 and after_qed =
-  AfterQed of (state -> state Seq.seq) * (theory -> theory);
+  AfterQed of
+   (thm list -> state -> state Seq.seq) *
+   (thm list * thm list -> theory -> theory);
 
 fun make_node (context, facts, mode, goal) =
   Node {context = context, facts = facts, mode = mode, goal = goal};
@@ -708,7 +710,7 @@
     val thy' = theory_of state';
 
     val AfterQed (after_local, after_global) = after_qed;
-    val after_qed' = AfterQed (after_local o map_context gen_binds, after_global);
+    val after_qed' = AfterQed (fn results => after_local results o map_context gen_binds, after_global);
 
     val props = List.concat propss;
     val cprop = Thm.cterm_of thy' (Logic.mk_conjunction_list props);
@@ -753,14 +755,14 @@
         locale_spec = (case raw_locale of NONE => NONE | SOME (_, x) => SOME (the opt_name, x)),
         view = view,
         export = export})
-      (AfterQed (Seq.single, after_global))
+      (AfterQed (K Seq.single, after_global))
       true (map (fst o fst) concl) propp
   end;
 
 fun local_goal' prepp kind (check: bool -> state -> state) after_local pr args int state =
   state
   |> setup_goal open_block prepp (K I) (kind (map (snd o fst) args))
-    (AfterQed (after_local, I)) pr (map (fst o fst) args) (map snd args)
+    (AfterQed (after_local, K I)) pr (map (fst o fst) args) (map snd args)
   |> warn_extra_tfrees state
   |> check int;
 
@@ -839,7 +841,7 @@
     |> (fn st => Seq.map (fn res =>
       note_thmss_i ((names ~~ attss) ~~ map (single o Thm.no_attributes) res) st) resultq)
     |> (Seq.flat o Seq.map opt_solve)
-    |> (Seq.flat o Seq.map after_local)
+    |> (Seq.flat o Seq.map (after_local results))
   end;
 
 fun local_qed finalize print state =
@@ -886,7 +888,7 @@
       |> (fn (thy, res) => (thy, res)
           |>> (#1 o Locale.smart_note_thmss k locale_name
             [((name, atts), [(List.concat (map #2 res), [])])]));
-  in (after_global theory', ((k, name), results')) end;
+  in (after_global (locale_results, results) theory', ((k, name), results')) end;
 
 
 (*note: clients should inspect first result only, as backtracking may destroy theory*)

--- a/src/Pure/axclass.ML	Mon Aug 08 22:11:31 2005 +0200
+++ b/src/Pure/axclass.ML	Mon Aug 08 22:14:04 2005 +0200
@@ -319,7 +319,7 @@
 
 fun inst_proof mk_prop add_thms inst int theory =
   theory
-  |> IsarThy.multi_theorem_i Drule.internalK I ProofContext.export_standard
+  |> IsarThy.multi_theorem_i Drule.internalK (K I) ProofContext.export_standard
     ("", [fn (thy, th) => (add_thms [th] thy, th)]) []
     (map (fn t => (("", []), [(t, ([], []))])) (mk_prop theory inst)) int;