--- a/src/Pure/codegen.ML Thu Apr 10 20:54:18 2008 +0200
+++ b/src/Pure/codegen.ML Sat Apr 12 17:00:35 2008 +0200
@@ -1074,8 +1074,8 @@
Logic.mk_equals (t, eval_term thy t);
fun evaluation_conv ct =
- let val {thy, t, ...} = rep_cterm ct
- in Thm.invoke_oracle_i thy "Pure.evaluation" (thy, Evaluation t) end;
+ let val thy = Thm.theory_of_cterm ct
+ in Thm.invoke_oracle_i thy "Pure.evaluation" (thy, Evaluation (Thm.term_of ct)) end;
val _ = Context.>> (Context.map_theory
(Theory.add_oracle ("evaluation", evaluation_oracle)));