# HG changeset patch
# User wenzelm
# Date 1160686649 -7200
# Node ID c879f0150db91c10e7b9b956dd0933aee2cb7f9d
# Parent  408f3a1cef2ea1b1df4dc49faae427004a3fe179
print_evaluated_term: Toplevel.context_of;

diff -r 408f3a1cef2e -r c879f0150db9 src/Pure/Tools/nbe.ML
--- 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*)
diff -r 408f3a1cef2e -r c879f0150db9 src/Pure/codegen.ML
--- 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