src/HOL/Predicate_Compile_Examples/Predicate_Compile_Tests.thy

   (o * o => bool) => i * o => bool,
   (o * o => bool) => o * i => bool,
   (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]
 declare Id_on_def[unfolded Bex_def UNION_eq singleton_iff, code_pred_def]