print_evaluated_term: Toplevel.context_of;

--- a/src/Pure/Tools/nbe.ML	Thu Oct 12 22:57:24 2006 +0200
+++ b/src/Pure/Tools/nbe.ML	Thu Oct 12 22:57:29 2006 +0200
@@ -190,7 +190,7 @@
 
 fun norm_print_term_e (modes, raw_t) state =
   let
-    val ctxt = (Proof.context_of o Toplevel.enter_forward_proof) state;
+    val ctxt = Context.proof_of (Toplevel.context_of state);
   in norm_print_term ctxt modes (ProofContext.read_term ctxt raw_t) end;
 
 end; (*local*)

--- a/src/Pure/codegen.ML	Thu Oct 12 22:57:24 2006 +0200
+++ b/src/Pure/codegen.ML	Thu Oct 12 22:57:29 2006 +0200
@@ -1050,9 +1050,9 @@
 
 fun print_evaluated_term s = Toplevel.keep (fn state =>
   let
-    val state' = Toplevel.enter_forward_proof state;
-    val ctxt = Proof.context_of state';
-    val t = eval_term (Proof.theory_of state') (ProofContext.read_term ctxt s);
+    val ctxt = Context.proof_of (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;
   in
     writeln (Pretty.string_of