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