1.1 --- a/src/Pure/Isar/isar_thy.ML	Tue May 31 11:53:33 2005 +0200
     1.2 +++ b/src/Pure/Isar/isar_thy.ML	Tue May 31 11:53:34 2005 +0200
     1.3 @@ -482,6 +482,23 @@
     1.4  
     1.5  (* global endings *)
     1.6  
     1.7 +fun name_results "" res = res
     1.8 +  | name_results name res =
     1.9 +      let
    1.10 +        val n = length (List.concat (map #2 res));
    1.11 +        fun name_res (i, (a, ths)) =
    1.12 +          let
    1.13 +            val m = length ths;
    1.14 +            val j = i + m;
    1.15 +          in
    1.16 +            if a <> "" then (j, (a, ths))
    1.17 +            else if m = n then (j, (name, ths))
    1.18 +            else if m = 1 then
    1.19 +              (j, (PureThy.string_of_thmref (name, SOME [PureThy.Single i]), ths))
    1.20 +            else (j, (PureThy.string_of_thmref (name, SOME [PureThy.FromTo (i, j - 1)]), ths))
    1.21 +          end;
    1.22 +      in #2 (foldl_map name_res (1, res)) end;
    1.23 +
    1.24  fun global_result finish = Toplevel.proof_to_theory' (fn int => fn prf =>
    1.25    let
    1.26      val state = ProofHistory.current prf;
    1.27 @@ -490,7 +507,7 @@
    1.28    in
    1.29      if kind = "" orelse kind = Drule.internalK then ()
    1.30      else (print_result (Proof.context_of state) ((kind, name), res);
    1.31 -      Context.setmp (SOME thy) (Present.results kind) res);
    1.32 +      Context.setmp (SOME thy) (Present.results kind) (name_results name res));
    1.33      thy
    1.34    end);
    1.35