# HG changeset patch
# User wenzelm
# Date 1221759590 -7200
# Node ID f15c2e2ffe1b2f317383f9163d69c56c8947a38a
# Parent  cad470c699355f9b533e8ef9d7eadb95a1d6db8a
eval_term: CRITICAL due to eval_result;
simplified oracle interface;

diff -r cad470c69935 -r f15c2e2ffe1b src/Pure/codegen.ML
--- a/src/Pure/codegen.ML	Thu Sep 18 19:39:49 2008 +0200
+++ b/src/Pure/codegen.ML	Thu Sep 18 19:39:50 2008 +0200
@@ -1039,18 +1039,17 @@
                 [str "(result ())"],
               str ");"]) ^
           "\n\nend;\n";
-        val _ = ML_Context.eval_in (SOME ctxt) false Position.none s;
+        val _ = NAMED_CRITICAL "codegen" (fn () =>
+          ML_Context.eval_in (SOME ctxt) false Position.none s);
       in !eval_result end;
   in e () end;
 
-exception Evaluation of term;
-
-fun evaluation_oracle (thy, Evaluation t) =
-  Logic.mk_equals (t, eval_term thy t);
-
-fun evaluation_conv ct =
-  let val thy = Thm.theory_of_cterm ct
-  in Thm.invoke_oracle_i thy "HOL.evaluation" (thy, Evaluation (Thm.term_of ct)) end;
+val (_, evaluation_conv) = Context.>>> (Context.map_theory_result
+  (Thm.add_oracle ("evaluation", fn ct =>
+    let
+      val thy = Thm.theory_of_cterm ct;
+      val t = Thm.term_of ct;
+    in Thm.cterm_of thy (Logic.mk_equals (t, eval_term thy t)) end)));
 
 
 (**** Interface ****)
@@ -1132,7 +1131,6 @@
 
 val setup = add_codegen "default" default_codegen
   #> add_tycodegen "default" default_tycodegen
-  #> Theory.add_oracle ("evaluation", evaluation_oracle)
   #> Value.add_evaluator ("SML", eval_term o ProofContext.theory_of)
   #> Code.add_attribute ("unfold", Scan.succeed (Thm.declaration_attribute
        (fn thm => Context.mapping (add_unfold thm #> Code.add_inline thm) I)));