| 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