src/Pure/Isar/proof_context.ML
changeset 28087 a9cccdd9d521
parent 28082 37350f301128
child 28209 02f3222a392d
     1.1 --- a/src/Pure/Isar/proof_context.ML	Tue Sep 02 18:01:23 2008 +0200
     1.2 +++ b/src/Pure/Isar/proof_context.ML	Tue Sep 02 18:01:24 2008 +0200
     1.3 @@ -296,10 +296,10 @@
     1.4    | pretty_thms ctxt ths = Pretty.blk (0, Pretty.fbreaks (map (pretty_thm ctxt) ths));
     1.5  
     1.6  fun pretty_fact ctxt ("", ths) = pretty_thms ctxt ths
     1.7 -  | pretty_fact ctxt (a, [th]) =
     1.8 -      Pretty.block [Pretty.str (a ^ ":"), Pretty.brk 1, pretty_thm ctxt th]
     1.9 -  | pretty_fact ctxt (a, ths) =
    1.10 -      Pretty.block (Pretty.fbreaks (Pretty.str (a ^ ":") :: map (pretty_thm ctxt) ths));
    1.11 +  | pretty_fact ctxt (a, [th]) = Pretty.block
    1.12 +      [Pretty.str (NameSpace.base a ^ ":"), Pretty.brk 1, pretty_thm ctxt th]
    1.13 +  | pretty_fact ctxt (a, ths) = Pretty.block
    1.14 +      (Pretty.fbreaks (Pretty.str (NameSpace.base a ^ ":") :: map (pretty_thm ctxt) ths));
    1.15  
    1.16  val string_of_thm = Pretty.string_of oo pretty_thm;
    1.17