# HG changeset patch
# User wenzelm
# Date 1165274956 -3600
# Node ID 5154a7213d3ccbe5aa8098e0c6142952b768742b
# Parent  bdf3e74727df7812d56366273982e2fcff77bf8f
notes: added non-official name;

diff -r bdf3e74727df -r 5154a7213d3c src/Pure/Isar/theory_target.ML
--- a/src/Pure/Isar/theory_target.ML	Tue Dec 05 00:29:13 2006 +0100
+++ b/src/Pure/Isar/theory_target.ML	Tue Dec 05 00:29:16 2006 +0100
@@ -183,7 +183,10 @@
       |> Drule.zero_var_indexes_list;
 
     (*thm definition*)
-    val result = PureThy.name_thm true (name, Goal.close_result th'');
+    val result = th''
+      |> PureThy.name_thm true true ""
+      |> Goal.close_result
+      |> PureThy.name_thm true true name;
 
     (*import fixes*)
     val (tvars, vars) =
@@ -202,7 +205,8 @@
       (case SINGLE (Seq.INTERVAL assm_tac 1 nprems) result' of
         NONE => raise THM ("Failed to re-import result", 0, [result'])
       | SOME res => res) COMP (concl_conv COMP_INCR Drule.equal_elim_rule2)
-      |> Goal.norm_result;
+      |> Goal.norm_result
+      |> PureThy.name_thm false false name;
 
   in (result'', result) end;