diff -r 94a794672c8b -r 26ead7ed4f4b src/HOL/Tools/recfun_codegen.ML
--- a/src/HOL/Tools/recfun_codegen.ML	Mon Feb 26 21:34:16 2007 +0100
+++ b/src/HOL/Tools/recfun_codegen.ML	Mon Feb 26 23:18:24 2007 +0100
@@ -24,7 +24,7 @@
   val empty = Symtab.empty;
   val copy = I;
   val extend = I;
-  fun merge _ = Symtab.merge_list (Drule.eq_thm_prop o pairself fst);
+  fun merge _ = Symtab.merge_list (Thm.eq_thm_prop o pairself fst);
   fun print _ _ = ();
 end);
 
@@ -56,7 +56,7 @@
   in case Symtab.lookup tab s of
       NONE => thy
     | SOME thms =>
-        RecCodegenData.put (Symtab.update (s, remove (eq_thm o apsnd fst) thm thms) tab) thy
+        RecCodegenData.put (Symtab.update (s, remove (Thm.eq_thm o apsnd fst) thm thms) tab) thy
   end handle TERM _ => (warn thm; thy);
 
 val del = Thm.declaration_attribute