diff -r 293934e41dfd -r d0d2af4db18f src/Pure/codegen.ML
--- 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));