# HG changeset patch
# User haftmann
# Date 1167937259 -3600
# Node ID a69d21fc6d68a89076cebd0ee7979cb762ab9c7f
# Parent  34e190b243993db890a656ba3898a7ca53c1f817
fixed eval oracle

diff -r 34e190b24399 -r a69d21fc6d68 src/HOL/Code_Generator.thy
--- a/src/HOL/Code_Generator.thy	Thu Jan 04 19:53:00 2007 +0100
+++ b/src/HOL/Code_Generator.thy	Thu Jan 04 20:00:59 2007 +0100
@@ -196,8 +196,8 @@
 ML {*
 signature HOL_EVAL =
 sig
-  val eval_ref: bool option ref
-  val eval_prop: theory -> term -> term
+  val reff: bool option ref
+  val prop: theory -> term -> term
   val tac: int -> tactic
   val method: Method.src -> Proof.context -> Method.method
 end;
@@ -205,19 +205,22 @@
 structure HOL_Eval =
 struct
 
-val eval_ref : bool option ref = ref NONE;
+val reff : bool option ref = ref NONE;
 
-fun eval_prop thy t =
+fun prop thy t =
   if CodegenPackage.eval_term thy
-    (("HOL_Eval.eval_ref", eval_ref), t)
+    (("HOL_Eval.reff", reff), t)
     then HOLogic.true_const
-    else HOLogic.false_const;
+    else HOLogic.false_const
+
+fun mk_eq thy t =
+  Logic.mk_equals (t, prop thy t)
 
 end;
 *}
 
 setup {*
-  PureThy.add_oracle ("invoke", "term", "HOL_Eval.eval_prop")
+  PureThy.add_oracle ("invoke", "term", "HOL_Eval.mk_eq")
 *}
 
 ML {*