--- a/src/HOL/Tools/BNF/bnf_lfp.ML Tue Mar 04 13:38:02 2014 +0100
+++ b/src/HOL/Tools/BNF/bnf_lfp.ML Tue Mar 04 18:57:17 2014 +0100
@@ -1825,8 +1825,8 @@
val common_notes =
[(ctor_inductN, [ctor_induct_thm]),
(ctor_induct2N, [ctor_induct2_thm]),
- (rel_inductN, [Irel_induct_thm]),
- (ctor_fold_transferN, ctor_fold_transfer_thms)]
+ (ctor_fold_transferN, ctor_fold_transfer_thms),
+ (ctor_rel_inductN, [Irel_induct_thm])]
|> map (fn (thmN, thms) =>
((Binding.qualify true (Binding.name_of b) (Binding.name thmN), []), [(thms, [])]));