src/Pure/codegen.ML
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;