--- a/src/HOL/Predicate_Compile_Examples/Predicate_Compile_Tests.thy Tue Apr 03 08:55:06 2012 +0200
+++ b/src/HOL/Predicate_Compile_Examples/Predicate_Compile_Tests.thy Tue Apr 03 17:26:30 2012 +0900
@@ -1027,8 +1027,8 @@
(o * o => bool) => i * i => bool) [inductify] converse .
thm converse.equation
-code_pred [inductify] rel_comp .
-thm rel_comp.equation
+code_pred [inductify] relcomp .
+thm relcomp.equation
code_pred [inductify] Image .
thm Image.equation
declare singleton_iff[code_pred_inline]