--- a/src/HOL/Orderings.thy Mon Oct 08 22:06:32 2007 +0200
+++ b/src/HOL/Orderings.thy Tue Oct 09 00:20:13 2007 +0200
@@ -275,9 +275,9 @@
let
val structs = Data.get (Context.Proof ctxt);
fun pretty_term t = Pretty.block
- [Pretty.quote (ProofContext.pretty_term ctxt t), Pretty.brk 1,
+ [Pretty.quote (Syntax.pretty_term ctxt t), Pretty.brk 1,
Pretty.str "::", Pretty.brk 1,
- Pretty.quote (ProofContext.pretty_typ ctxt (type_of t))];
+ Pretty.quote (Syntax.pretty_typ ctxt (type_of t))];
fun pretty_struct ((s, ts), _) = Pretty.block
[Pretty.str s, Pretty.str ":", Pretty.brk 1,
Pretty.enclose "(" ")" (Pretty.breaks (map pretty_term ts))];