--- a/src/Pure/codegen.ML Wed Apr 04 20:22:32 2007 +0200
+++ b/src/Pure/codegen.ML Wed Apr 04 23:29:33 2007 +0200
@@ -1064,8 +1064,8 @@
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;
+ let val {thy, t, ...} = rep_cterm ct
+ in Thm.invoke_oracle_i thy "Pure.evaluation" (thy, Evaluation t) end;
val _ = Context.add_setup
(Theory.add_oracle ("evaluation", evaluation_oracle));