# HG changeset patch
# User wenzelm
# Date 1221209640 -7200
# Node ID 02f3222a392d23362b0efa83bff7f16c2d2f909b
# Parent  3a8b3453129a15392d033403245b5243fd8a33c1
pretty_fact: extern fact name wrt. the given context, assuming that is the proper one for presentation;

diff -r 3a8b3453129a -r 02f3222a392d src/Pure/Isar/proof_context.ML
--- a/src/Pure/Isar/proof_context.ML	Thu Sep 11 22:22:59 2008 +0200
+++ b/src/Pure/Isar/proof_context.ML	Fri Sep 12 10:54:00 2008 +0200
@@ -295,11 +295,13 @@
 fun pretty_thms ctxt [th] = pretty_thm ctxt th
   | pretty_thms ctxt ths = Pretty.blk (0, Pretty.fbreaks (map (pretty_thm ctxt) ths));
 
+val extern_fact = Facts.extern o facts_of;
+
 fun pretty_fact ctxt ("", ths) = pretty_thms ctxt ths
   | pretty_fact ctxt (a, [th]) = Pretty.block
-      [Pretty.str (NameSpace.base a ^ ":"), Pretty.brk 1, pretty_thm ctxt th]
+      [Pretty.str (extern_fact ctxt a ^ ":"), Pretty.brk 1, pretty_thm ctxt th]
   | pretty_fact ctxt (a, ths) = Pretty.block
-      (Pretty.fbreaks (Pretty.str (NameSpace.base a ^ ":") :: map (pretty_thm ctxt) ths));
+      (Pretty.fbreaks (Pretty.str (extern_fact ctxt a ^ ":") :: map (pretty_thm ctxt) ths));
 
 val string_of_thm = Pretty.string_of oo pretty_thm;