new-style oracle setup

--- a/src/HOL/Code_Generator.thy	Mon Dec 18 08:21:24 2006 +0100
+++ b/src/HOL/Code_Generator.thy	Mon Dec 18 08:21:25 2006 +0100
@@ -116,31 +116,39 @@
 signature HOL_EVAL =
 sig
   val eval_ref: bool option ref
-  val oracle: string * (theory * exn -> term)
+  val eval_prop: theory -> term -> term
   val tac: int -> tactic
   val method: Method.src -> Proof.context -> Method.method
 end;
 
-structure HOLEval : HOL_EVAL =
+structure HOL_Eval =
 struct
 
 val eval_ref : bool option ref = ref NONE;
 
 fun eval_prop thy t =
-  CodegenPackage.eval_term
-    thy (("HOLEval.eval_ref", eval_ref), t);
+  if CodegenPackage.eval_term thy
+    (("HOL_Eval.eval_ref", eval_ref), t)
+    then HOLogic.true_const
+    else HOLogic.false_const;
 
-exception Eval of term;
+end;
+*}
 
-val oracle = ("Eval", fn (thy, Eval t) =>
-  Logic.mk_equals (t, if eval_prop thy t then HOLogic.true_const else HOLogic.false_const));
+setup {*
+  PureThy.add_oracle ("invoke", "term", "HOL_Eval.eval_prop")
+*}
 
-val oracle_name = Sign.full_name (the_context ()) (fst oracle);
+ML {*
+structure HOL_Eval : HOL_EVAL =
+struct
+
+open HOL_Eval;
 
 fun conv ct =
   let
     val {thy, t, ...} = rep_cterm ct;
-  in Thm.invoke_oracle_i thy oracle_name (thy, Eval t) end;
+  in invoke thy t end;
 
 fun tac i = Tactical.PRIMITIVE (Drule.fconv_rule
   (Drule.goals_conv (equal i) (HOLogic.Trueprop_conv conv)));
@@ -152,8 +160,7 @@
 *}
 
 setup {*
-  Theory.add_oracle HOLEval.oracle
-  #> Method.add_method ("eval", HOLEval.method, "solve goal by evaluation")
+  Method.add_method ("eval", HOL_Eval.method, "solve goal by evaluation")
 *}