src/Pure/codegen.ML
changeset 24508 c8b82fec6447
parent 24469 01fd2863d7c8
child 24565 08578e380a41
--- 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