print_evaluated_term: Toplevel.context_of;
authorwenzelm
Thu Oct 12 22:57:29 2006 +0200 (2006-10-12 ago)
changeset 21002c879f0150db9
parent 21001 408f3a1cef2e
child 21003 37492b0062c6
print_evaluated_term: Toplevel.context_of;
src/Pure/Tools/nbe.ML
src/Pure/codegen.ML
     1.1 --- a/src/Pure/Tools/nbe.ML	Thu Oct 12 22:57:24 2006 +0200
     1.2 +++ b/src/Pure/Tools/nbe.ML	Thu Oct 12 22:57:29 2006 +0200
     1.3 @@ -190,7 +190,7 @@
     1.4  
     1.5  fun norm_print_term_e (modes, raw_t) state =
     1.6    let
     1.7 -    val ctxt = (Proof.context_of o Toplevel.enter_forward_proof) state;
     1.8 +    val ctxt = Context.proof_of (Toplevel.context_of state);
     1.9    in norm_print_term ctxt modes (ProofContext.read_term ctxt raw_t) end;
    1.10  
    1.11  end; (*local*)
     2.1 --- a/src/Pure/codegen.ML	Thu Oct 12 22:57:24 2006 +0200
     2.2 +++ b/src/Pure/codegen.ML	Thu Oct 12 22:57:29 2006 +0200
     2.3 @@ -1050,9 +1050,9 @@
     2.4  
     2.5  fun print_evaluated_term s = Toplevel.keep (fn state =>
     2.6    let
     2.7 -    val state' = Toplevel.enter_forward_proof state;
     2.8 -    val ctxt = Proof.context_of state';
     2.9 -    val t = eval_term (Proof.theory_of state') (ProofContext.read_term ctxt s);
    2.10 +    val ctxt = Context.proof_of (Toplevel.context_of state);
    2.11 +    val thy = ProofContext.theory_of ctxt;
    2.12 +    val t = eval_term thy (ProofContext.read_term ctxt s);
    2.13      val T = Term.type_of t;
    2.14    in
    2.15      writeln (Pretty.string_of