explicit context for Codegen.eval_term etc.;

--- a/src/HOL/HOL.thy	Wed Apr 20 13:54:07 2011 +0200
+++ b/src/HOL/HOL.thy	Wed Apr 20 14:33:33 2011 +0200
@@ -1969,20 +1969,22 @@
 subsubsection {* Evaluation and normalization by evaluation *}
 
 setup {*
-  Value.add_evaluator ("SML", Codegen.eval_term o Proof_Context.theory_of)  (* FIXME proper context!? *)
+  Value.add_evaluator ("SML", Codegen.eval_term)
 *}
 
 ML {*
 fun gen_eval_method conv ctxt = SIMPLE_METHOD'
-  (CONVERSION (Conv.params_conv (~1) (K (Conv.concl_conv (~1) (conv (Proof_Context.theory_of ctxt)))) ctxt)
+  (CONVERSION (Conv.params_conv ~1 (K (Conv.concl_conv ~1 (conv ctxt))) ctxt)
     THEN' rtac TrueI)
 *}
 
-method_setup eval = {* Scan.succeed (gen_eval_method Code_Runtime.dynamic_holds_conv) *}
-  "solve goal by evaluation"
+method_setup eval = {*
+  Scan.succeed (gen_eval_method (Code_Runtime.dynamic_holds_conv o Proof_Context.theory_of))
+*} "solve goal by evaluation"
 
-method_setup evaluation = {* Scan.succeed (gen_eval_method (K Codegen.evaluation_conv)) *}
-  "solve goal by evaluation"
+method_setup evaluation = {*
+  Scan.succeed (gen_eval_method Codegen.evaluation_conv)
+*} "solve goal by evaluation"
 
 method_setup normalization = {*
   Scan.succeed (fn ctxt => SIMPLE_METHOD'

--- a/src/HOL/Library/reflection.ML	Wed Apr 20 13:54:07 2011 +0200
+++ b/src/HOL/Library/reflection.ML	Wed Apr 20 14:33:33 2011 +0200
@@ -312,7 +312,7 @@
     val th = genreflect ctxt conv corr_thms raw_eqs t RS ssubst
   in rtac th i THEN TRY (rtac TrueI i) end);  (* FIXME THEN_ALL_NEW !? *)
 
-fun reflection_tac ctxt = gen_reflection_tac ctxt Codegen.evaluation_conv;
+fun reflection_tac ctxt = gen_reflection_tac ctxt (Codegen.evaluation_conv ctxt);
   (*FIXME why Codegen.evaluation_conv?  very specific...*)
 
 end

--- a/src/Pure/codegen.ML	Wed Apr 20 13:54:07 2011 +0200
+++ b/src/Pure/codegen.ML	Wed Apr 20 14:33:33 2011 +0200
@@ -77,8 +77,8 @@
   val test_fn: (int -> term list option) Unsynchronized.ref  (* FIXME *)
   val test_term: Proof.context -> term -> int -> term list option
   val eval_result: (unit -> term) Unsynchronized.ref  (* FIXME *)
-  val eval_term: theory -> term -> term
-  val evaluation_conv: cterm -> thm
+  val eval_term: Proof.context -> term -> term
+  val evaluation_conv: Proof.context -> conv
   val parse_mixfix: (string -> 'a) -> string -> 'a mixfix list
   val quotes_of: 'a mixfix list -> 'a list
   val num_args_of: 'a mixfix list -> int
@@ -903,11 +903,11 @@
 
 val eval_result = Unsynchronized.ref (fn () => Bound 0);
 
-fun eval_term thy t =
+fun eval_term ctxt t =
   let
-    val ctxt = Proof_Context.init_global thy;  (* FIXME *)
     val e =
       let
+        val thy = Proof_Context.theory_of ctxt;
         val _ = (null (Term.add_tvars t []) andalso null (Term.add_tfrees t [])) orelse
           error "Term to be evaluated contains type variables";
         val _ = (null (Term.add_vars t []) andalso null (Term.add_frees t [])) orelse
@@ -930,12 +930,18 @@
       end
   in e () end;
 
-val (_, evaluation_conv) = Context.>>> (Context.map_theory_result
-  (Thm.add_oracle (Binding.name "evaluation", fn ct =>
+val (_, evaluation_oracle) = Context.>>> (Context.map_theory_result
+  (Thm.add_oracle (Binding.name "evaluation", fn (ctxt, ct) =>
     let
-      val thy = Thm.theory_of_cterm ct;
+      val thy = Proof_Context.theory_of ctxt;
       val t = Thm.term_of ct;
-    in Thm.cterm_of thy (Logic.mk_equals (t, eval_term thy t)) end)));
+    in
+      if Theory.subthy (Thm.theory_of_cterm ct, thy) then
+        Thm.cterm_of thy (Logic.mk_equals (t, eval_term ctxt t))
+      else raise CTERM ("evaluation_oracle: bad theory", [ct])
+    end)));
+
+fun evaluation_conv ctxt ct = evaluation_oracle (ctxt, ct);
 
 
 (**** Interface ****)