--- a/src/HOL/Tools/recfun_codegen.ML Sat Aug 28 20:24:40 2010 +0800
+++ b/src/HOL/Tools/recfun_codegen.ML Sat Aug 28 16:14:32 2010 +0200
@@ -40,7 +40,7 @@
end
| avoid_value thy thms = thms;
-fun get_equations thy defs (raw_c, T) = if raw_c = @{const_name "op ="} then ([], "") else
+fun get_equations thy defs (raw_c, T) = if raw_c = @{const_name HOL.eq} then ([], "") else
let
val c = AxClass.unoverload_const thy (raw_c, T);
val raw_thms = Code.get_cert thy (Code_Preproc.preprocess_functrans thy) c