# HG changeset patch
# User wenzelm
# Date 1164904943 -3600
# Node ID 1bd558879c440ff5e352a77e728266e81ccc4fab
# Parent  89105c15b43643d0411260894ddc254d2bb0b029
notes: proper naming of thm proof, activated import_export_proof;

diff -r 89105c15b436 -r 1bd558879c44 src/Pure/Isar/theory_target.ML
--- a/src/Pure/Isar/theory_target.ML	Thu Nov 30 17:42:21 2006 +0100
+++ b/src/Pure/Isar/theory_target.ML	Thu Nov 30 17:42:23 2006 +0100
@@ -206,21 +206,15 @@
 
   in (result'', result) end;
 
-fun import_export ctxt (_, raw_th) =
-  let
-    val thy_ctxt = ProofContext.init (ProofContext.theory_of ctxt);
-    val result'' = Goal.norm_result raw_th;
-    val result = Goal.norm_result (singleton (ProofContext.export ctxt thy_ctxt) result'');
-  in (result'', result) end;
-
 fun notes loc kind facts lthy =
   let
     val is_loc = loc <> "";
     val thy = ProofContext.theory_of lthy;
+    val full = LocalTheory.full_name lthy;
 
     val facts' = facts
-      |> map (fn (a, bs) => (a, PureThy.burrow_fact (PureThy.name_multi (fst a)) bs))
-      |> PureThy.map_facts (import_export lthy);   (* FIXME import_export_proof *)
+      |> map (fn (a, bs) => (a, PureThy.burrow_fact (PureThy.name_multi (full (fst a))) bs))
+      |> PureThy.map_facts (import_export_proof lthy);
     val local_facts = PureThy.map_facts #1 facts'
       |> Attrib.map_facts (Attrib.attribute_i thy);
     val target_facts = PureThy.map_facts #1 facts'