--- a/src/Pure/Isar/proof_context.ML Tue Sep 02 18:01:23 2008 +0200
+++ b/src/Pure/Isar/proof_context.ML Tue Sep 02 18:01:24 2008 +0200
@@ -296,10 +296,10 @@
| pretty_thms ctxt ths = Pretty.blk (0, Pretty.fbreaks (map (pretty_thm ctxt) ths));
fun pretty_fact ctxt ("", ths) = pretty_thms ctxt ths
- | pretty_fact ctxt (a, [th]) =
- Pretty.block [Pretty.str (a ^ ":"), Pretty.brk 1, pretty_thm ctxt th]
- | pretty_fact ctxt (a, ths) =
- Pretty.block (Pretty.fbreaks (Pretty.str (a ^ ":") :: map (pretty_thm ctxt) ths));
+ | pretty_fact ctxt (a, [th]) = Pretty.block
+ [Pretty.str (NameSpace.base 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));
val string_of_thm = Pretty.string_of oo pretty_thm;