1.1 --- a/src/Pure/codegen.ML	Mon Oct 08 22:06:32 2007 +0200
     1.2 +++ b/src/Pure/codegen.ML	Tue Oct 09 00:20:13 2007 +0200
     1.3 @@ -982,8 +982,7 @@
     1.4    | pretty_counterex ctxt (SOME cex) =
     1.5        Pretty.chunks (Pretty.str "Counterexample found:\n" ::
     1.6          map (fn (s, t) =>
     1.7 -          Pretty.block [Pretty.str (s ^ " ="), Pretty.brk 1,
     1.8 -            ProofContext.pretty_term ctxt t]) cex);
     1.9 +          Pretty.block [Pretty.str (s ^ " ="), Pretty.brk 1, Syntax.pretty_term ctxt t]) cex);
    1.10  
    1.11  val auto_quickcheck = ref true;
    1.12  val auto_quickcheck_time_limit = ref 5000;
    1.13 @@ -1043,8 +1042,8 @@
    1.14      val T = Term.type_of t;
    1.15    in
    1.16      Pretty.writeln
    1.17 -      (Pretty.block [Pretty.quote (ProofContext.pretty_term ctxt t), Pretty.fbrk,
    1.18 -        Pretty.str "::", Pretty.brk 1, Pretty.quote (ProofContext.pretty_typ ctxt T)])
    1.19 +      (Pretty.block [Pretty.quote (Syntax.pretty_term ctxt t), Pretty.fbrk,
    1.20 +        Pretty.str "::", Pretty.brk 1, Pretty.quote (Syntax.pretty_typ ctxt T)])
    1.21    end);
    1.22  
    1.23  exception Evaluation of term;