changeset 21506 | b2a673894ce5 |
parent 21478 | a90250b1cf42 |
child 21719 | b67fbfc8a126 |
--- a/src/Pure/codegen.ML Thu Nov 23 22:38:29 2006 +0100 +++ b/src/Pure/codegen.ML Thu Nov 23 22:38:30 2006 +0100 @@ -1048,7 +1048,7 @@ fun print_evaluated_term s = Toplevel.keep (fn state => let - val ctxt = Context.proof_of (Toplevel.context_of state); + val ctxt = Toplevel.context_of state; val thy = ProofContext.theory_of ctxt; val t = eval_term thy (ProofContext.read_term ctxt s); val T = Term.type_of t;