diff -r ac22a2a67100 -r c8b82fec6447 src/Pure/codegen.ML
--- a/src/Pure/codegen.ML	Sat Sep 01 01:22:11 2007 +0200
+++ b/src/Pure/codegen.ML	Sat Sep 01 15:46:59 2007 +0200
@@ -1024,7 +1024,7 @@
   let
     val ctxt = Toplevel.context_of state;
     val thy = ProofContext.theory_of ctxt;
-    val t = eval_term thy (ProofContext.read_term ctxt s);
+    val t = eval_term thy (Syntax.read_term ctxt s);
     val T = Term.type_of t;
   in
     writeln (Pretty.string_of