diff -r ad3a8569759c -r 2a45e400fdad src/Pure/codegen.ML
--- a/src/Pure/codegen.ML	Mon Oct 08 22:06:32 2007 +0200
+++ b/src/Pure/codegen.ML	Tue Oct 09 00:20:13 2007 +0200
@@ -982,8 +982,7 @@
   | pretty_counterex ctxt (SOME cex) =
       Pretty.chunks (Pretty.str "Counterexample found:\n" ::
         map (fn (s, t) =>
-          Pretty.block [Pretty.str (s ^ " ="), Pretty.brk 1,
-            ProofContext.pretty_term ctxt t]) cex);
+          Pretty.block [Pretty.str (s ^ " ="), Pretty.brk 1, Syntax.pretty_term ctxt t]) cex);
 
 val auto_quickcheck = ref true;
 val auto_quickcheck_time_limit = ref 5000;
@@ -1043,8 +1042,8 @@
     val T = Term.type_of t;
   in
     Pretty.writeln
-      (Pretty.block [Pretty.quote (ProofContext.pretty_term ctxt t), Pretty.fbrk,
-        Pretty.str "::", Pretty.brk 1, Pretty.quote (ProofContext.pretty_typ ctxt T)])
+      (Pretty.block [Pretty.quote (Syntax.pretty_term ctxt t), Pretty.fbrk,
+        Pretty.str "::", Pretty.brk 1, Pretty.quote (Syntax.pretty_typ ctxt T)])
   end);
 
 exception Evaluation of term;