# HG changeset patch
# User haftmann
# Date 1158672144 -7200
# Node ID 65bd267ae23f3db948ac2e4d4530151b81ea9b57
# Parent  f8031b91c9460424d698442c724aff2b87d36b38
moved base setup for evaluation oracle hier

diff -r f8031b91c946 -r 65bd267ae23f src/Pure/codegen.ML
--- a/src/Pure/codegen.ML	Tue Sep 19 15:22:21 2006 +0200
+++ b/src/Pure/codegen.ML	Tue Sep 19 15:22:24 2006 +0200
@@ -77,6 +77,7 @@
   val test_term: theory -> int -> int -> term -> (string * term) list option
   val eval_result: term ref
   val eval_term: theory -> term -> term
+  val evaluation_conv: cterm -> thm
   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
@@ -1059,6 +1060,17 @@
         Pretty.str "::", Pretty.brk 1, Pretty.quote (ProofContext.pretty_typ ctxt T)]))
   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 {sign, t, ...} = rep_cterm ct
+  in Thm.invoke_oracle_i sign "Pure.Evaluation" (sign, Evaluation t) end;
+
+val _ = Context.add_setup
+  (Theory.add_oracle ("Evaluation", evaluation_oracle));
 
 (**** Interface ****)