# HG changeset patch
# User wenzelm
# Date 1117533214 -7200
# Node ID ee6f7e6fc196f9b812287a2a050d0629caa1a632
# Parent  8eead5356ccb43ab5b57231272da1cb87f175513
improved naming of complex theorems in presentation;

diff -r 8eead5356ccb -r ee6f7e6fc196 src/Pure/Isar/isar_thy.ML
--- a/src/Pure/Isar/isar_thy.ML	Tue May 31 11:53:33 2005 +0200
+++ b/src/Pure/Isar/isar_thy.ML	Tue May 31 11:53:34 2005 +0200
@@ -482,6 +482,23 @@
 
 (* global endings *)
 
+fun name_results "" res = res
+  | name_results name res =
+      let
+        val n = length (List.concat (map #2 res));
+        fun name_res (i, (a, ths)) =
+          let
+            val m = length ths;
+            val j = i + m;
+          in
+            if a <> "" then (j, (a, ths))
+            else if m = n then (j, (name, ths))
+            else if m = 1 then
+              (j, (PureThy.string_of_thmref (name, SOME [PureThy.Single i]), ths))
+            else (j, (PureThy.string_of_thmref (name, SOME [PureThy.FromTo (i, j - 1)]), ths))
+          end;
+      in #2 (foldl_map name_res (1, res)) end;
+
 fun global_result finish = Toplevel.proof_to_theory' (fn int => fn prf =>
   let
     val state = ProofHistory.current prf;
@@ -490,7 +507,7 @@
   in
     if kind = "" orelse kind = Drule.internalK then ()
     else (print_result (Proof.context_of state) ((kind, name), res);
-      Context.setmp (SOME thy) (Present.results kind) res);
+      Context.setmp (SOME thy) (Present.results kind) (name_results name res));
     thy
   end);