--- a/src/Pure/Isar/args.ML Mon Oct 08 22:06:32 2007 +0200
+++ b/src/Pure/Isar/args.ML Tue Oct 09 00:20:13 2007 +0200
@@ -170,8 +170,8 @@
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 (Typ T)))) = Syntax.pretty_typ ctxt T
+ | prt (Arg (_, Value (SOME (Term t)))) = Syntax.pretty_term ctxt t
| prt (Arg (_, Value (SOME (Fact ths)))) =
Pretty.enclose "(" ")" (Pretty.breaks (map prt_thm ths))
| prt arg = Pretty.str (string_of arg);