src/Pure/Isar/proof.ML

   val at_bottom: state -> bool
   val local_qed: (state -> state Seq.seq)
     -> (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
 end;
 

       theory_of state
       |> locale_prefix locale (PureThy.have_thmss [Drule.kind k]
           ((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 =
   state
   |> end_proof true