--- a/src/Pure/Isar/args.ML Thu Dec 07 17:58:46 2006 +0100
+++ b/src/Pure/Isar/args.ML Thu Dec 07 17:58:48 2006 +0100
@@ -164,10 +164,12 @@
fun pretty_src ctxt src =
let
+ val prt_thm = Pretty.backquote o ProofContext.pretty_thm ctxt;
fun prt (Arg (_, Value (SOME (Text s)))) = Pretty.str (quote s)
| prt (Arg (_, Value (SOME (Typ T)))) = ProofContext.pretty_typ ctxt T
| prt (Arg (_, Value (SOME (Term t)))) = ProofContext.pretty_term ctxt t
- | prt (Arg (_, Value (SOME (Fact ths)))) = ProofContext.pretty_thms ctxt ths
+ | prt (Arg (_, Value (SOME (Fact ths)))) =
+ Pretty.enclose "(" ")" (Pretty.breaks (map prt_thm ths))
| prt arg = Pretty.str (string_of arg);
val (s, args) = #1 (dest_src src);
in Pretty.block (Pretty.breaks (Pretty.str s :: map prt args)) end;