pretty_fact: extern fact name wrt. the given context, assuming that is the proper one for presentation;
authorwenzelm
Fri, 12 Sep 2008 10:54:00 +0200
changeset 28209 02f3222a392d
parent 28208 3a8b3453129a
child 28210 c164d1892553
pretty_fact: extern fact name wrt. the given context, assuming that is the proper one for presentation;
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;