improved treatment of common result name;

--- a/src/Pure/Isar/isar_syn.ML	Mon Nov 19 20:47:57 2001 +0100
+++ b/src/Pure/Isar/isar_syn.ML	Mon Nov 19 23:37:01 2001 +0100
@@ -297,14 +297,16 @@
 (* statements *)
 
 val in_locale_elems =
-  Scan.option ((P.$$$ "(" -- P.$$$ "in") |-- P.xname -- P.opt_attribs --| P.$$$ ")") --
-  Scan.optional (P.$$$ "(" |-- P.!!! (Scan.repeat1 P.locale_element --| P.$$$ ")")) [];
+  Scan.option ((P.$$$ "(" -- P.$$$ "in") |-- P.!!! (P.xname -- P.opt_attribs --| P.$$$ ")")) --
+  Scan.optional (P.$$$ "(" |-- Scan.repeat1 P.locale_element --| P.!!! (P.$$$ ")")) [];
 
 val statement = P.and_list1 (P.opt_thm_name ":" -- Scan.repeat1 P.propp -- P.marg_comment);
+val statement' = P.$$$ "(" |-- statement --| P.!!! (P.$$$ ")") || statement;
 
 fun gen_theorem k =
   OuterSyntax.command k ("state " ^ k) K.thy_goal
-    (P.opt_thm_name ":" -- in_locale_elems -- statement >> (fn ((x, y), z) =>
+    (Scan.optional (P.thm_name ":" --| Scan.ahead (P.$$$ "(")) ("", [])
+      -- in_locale_elems -- statement' >> (fn ((x, y), z) =>
       (Toplevel.print o Toplevel.theory_to_proof (IsarThy.multi_theorem k x y z))));
 
 val theoremP = gen_theorem Drule.theoremK;

--- a/src/Pure/Isar/isar_thy.ML	Mon Nov 19 20:47:57 2001 +0100
+++ b/src/Pure/Isar/isar_thy.ML	Mon Nov 19 23:37:01 2001 +0100
@@ -203,6 +203,7 @@
 struct
 
 
+
 (** derived theory and proof operations **)
 
 (* markup commands *)
@@ -382,13 +383,18 @@
 
 local
 
-fun pretty_result ctxt k (name, ths) = Pretty.block
-  [Pretty.str (k ^ (if name = "" then "" else " " ^ name ^ ":")), Pretty.brk 1,
-    ProofContext.pretty_thms ctxt ths];
+fun prt_fact ctxt ("", ths) = ProofContext.pretty_thms ctxt ths
+  | prt_fact ctxt (name, ths) =
+      Pretty.block [Pretty.str (name ^ ":"), Pretty.brk 1, ProofContext.pretty_thms ctxt ths];
 
-fun pretty_results ctxt (kind, r :: rs) =
-      pretty_result ctxt kind r :: map (pretty_result ctxt "and") rs
-  | pretty_results _ (_, []) = [];
+fun prt_facts ctxt =
+  flat o (separate [Pretty.fbrk, Pretty.str "and "]) o map (single o prt_fact ctxt);
+
+fun pretty_results ctxt ((kind, ""), facts) =
+      Pretty.block (Pretty.str kind :: Pretty.brk 1 :: prt_facts ctxt facts)
+  | pretty_results ctxt ((kind, name), facts) = Pretty.blk (1,
+      [Pretty.str (kind ^ " " ^ name ^ ":"), Pretty.fbrk,
+        Pretty.blk (1, Pretty.str "(" :: prt_facts ctxt facts @ [Pretty.str ")"])]);
 
 fun pretty_rule s ctxt thm =
   Pretty.block [Pretty.str (s ^ " to solve goal by exported rule:"),
@@ -396,10 +402,11 @@
 
 in
 
-val print_result = (Pretty.writeln o Pretty.chunks) oo pretty_results;
+val print_result = Pretty.writeln oo pretty_results;
+fun print_result' ctxt (k, res) = print_result ctxt ((k, ""), res);
 
 fun cond_print_result_rule int =
-  if int then (print_result, priority oo (Pretty.string_of oo pretty_rule "Attempt"))
+  if int then (print_result', priority oo (Pretty.string_of oo pretty_rule "Attempt"))
   else (K (K ()), K (K ()));
 
 fun proof'' f = Toplevel.proof' (f o cond_print_result_rule);
@@ -422,7 +429,7 @@
           |> Library.transform_error;
         val result = (check (), None) handle Interrupt => raise Interrupt | e => (None, Some e);
       in (case result of (Some _, None) => () | (_, exn) => warn exn); state end;
-      
+
 end;
 
 
@@ -536,10 +543,10 @@
   let
     val state = ProofHistory.current prf;
     val _ = if Proof.at_bottom state then () else raise Toplevel.UNDEF;
-    val (thy, (kind, res)) = finish state;
+    val (thy, ((kind, name), res)) = finish state;
   in
     if kind = "" orelse kind = Drule.internalK then ()
-    else (print_result (Proof.context_of state) (kind, res);
+    else (print_result (Proof.context_of state) ((kind, name), res);
       Context.setmp (Some thy) Present.multi_result (kind, res));
     thy
   end);

--- a/src/Pure/Isar/method.ML	Mon Nov 19 20:47:57 2001 +0100
+++ b/src/Pure/Isar/method.ML	Mon Nov 19 23:37:01 2001 +0100
@@ -115,12 +115,13 @@
   val local_done_proof: (Proof.context -> string * (string * thm list) list -> unit) *
     (Proof.context -> thm -> unit) -> Proof.state -> Proof.state Seq.seq
   val global_qed: bool -> text option
-    -> Proof.state -> theory * (string * (string * thm list) list)
+    -> Proof.state -> theory * ((string * string) * (string * thm list) list)
   val global_terminal_proof: text * text option
-    -> Proof.state -> theory * (string * (string * thm list) list)
-  val global_default_proof: Proof.state -> theory * (string * (string * thm list) list)
-  val global_immediate_proof: Proof.state -> theory * (string * (string * thm list) list)
-  val global_done_proof: Proof.state -> theory * (string * (string * thm list) list)
+    -> Proof.state -> theory * ((string * string) * (string * thm list) list)
+  val global_default_proof: Proof.state -> theory * ((string * string) * (string * thm list) list)
+  val global_immediate_proof: Proof.state ->
+    theory * ((string * string) * (string * thm list) list)
+  val global_done_proof: Proof.state -> theory * ((string * string) * (string * thm list) list)
   val goal_args: (Args.T list -> 'a * Args.T list) -> ('a -> int -> tactic)
     -> Args.src -> Proof.context -> Proof.method
   val goal_args': (Proof.context * Args.T list -> 'a * (Proof.context * Args.T list))

--- a/src/Pure/Isar/proof.ML	Mon Nov 19 20:47:57 2001 +0100
+++ b/src/Pure/Isar/proof.ML	Mon Nov 19 23:37:01 2001 +0100
@@ -109,7 +109,7 @@
     -> (context -> string * (string * thm list) list -> unit) * (context -> thm -> unit)
     -> state -> state Seq.seq
   val global_qed: (state -> state Seq.seq) -> state
-    -> (theory * (string * (string * thm list) list)) Seq.seq
+    -> (theory * ((string * string) * (string * thm list) list)) Seq.seq
   val begin_block: state -> state
   val end_block: state -> state Seq.seq
   val next_block: state -> state
@@ -789,7 +789,7 @@
           ((names ~~ attss) ~~ map (single o Thm.no_attributes) (Library.unflat tss results)))
       |>> locale_add_thmss locale (names ~~ Library.unflat tss locale_results);
     val thy2 = thy1 |> PureThy.add_thmss [((cname, flat (map #2 res')), catts)] |> #1;
-  in (thy2, (k, res')) end;
+  in (thy2, ((k, cname), res')) end;
 
 (*note: clients should inspect first result only, as backtracking may destroy theory*)
 fun global_qed finalize state =

--- a/src/Pure/Isar/skip_proof.ML	Mon Nov 19 20:47:57 2001 +0100
+++ b/src/Pure/Isar/skip_proof.ML	Mon Nov 19 23:37:01 2001 +0100
@@ -14,7 +14,7 @@
   val prove: theory -> string list -> term list -> term -> (thm list -> tactic) -> thm
   val local_skip_proof: (Proof.context -> string * (string * thm list) list -> unit) *
     (Proof.context -> thm -> unit) -> Proof.state -> Proof.state Seq.seq
-  val global_skip_proof: Proof.state -> theory * (string * (string * thm list) list)
+  val global_skip_proof: Proof.state -> theory * ((string * string) * (string * thm list) list)
   val setup: (theory -> theory) list
 end;