# HG changeset patch
# User wenzelm
# Date 1214057932 -7200
# Node ID 5d24085e085809f74e257f003a0073507580e8b1
# Parent  fce7f0c7cf7685bf3c71bf425193eaa506bc5752
import_export_proof: simplified thm definition -- PureThy.name_thm does the job;

diff -r fce7f0c7cf76 -r 5d24085e0858 src/Pure/Isar/theory_target.ML
--- a/src/Pure/Isar/theory_target.ML	Sat Jun 21 16:18:51 2008 +0200
+++ b/src/Pure/Isar/theory_target.ML	Sat Jun 21 16:18:52 2008 +0200
@@ -117,10 +117,7 @@
       |> Drule.zero_var_indexes_list;
 
     (*thm definition*)
-    val result = th''
-      |> PureThy.name_thm true true ""
-      |> fold PureThy.tag_rule (Position.properties_of (Position.thread_data ()))
-      |> PureThy.name_thm true true name;
+    val result = PureThy.name_thm true true name th'';
 
     (*import fixes*)
     val (tvars, vars) =