import_export_proof: simplified thm definition -- PureThy.name_thm does the job;

--- 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) =