src/HOL/Tools/BNF/bnf_fp_def_sugar.ML

       val other_half_rel_distinct_thmss =
         map (map mk_other_half_rel_distinct_thm) half_rel_distinct_thmss;
       val (rel_distinct_thms, _) =
         join_halves n half_rel_distinct_thmss other_half_rel_distinct_thmss;
 
-      val rel_eq_thms =
+      val rel_code_thms =
         map (fn thm => thm RS @{thm eq_False[THEN iffD2]}) rel_distinct_thms @
         map2 (fn thm => fn 0 => thm RS @{thm eq_True[THEN iffD2]} | _ => thm) rel_inject_thms ms;
 
       val ctr_transfer_thms =
         let val goals = map2 (mk_parametricity_goal names_lthy Rs) ctrAs ctrBs in

         end;
 
       val code_attrs = if plugins code_plugin then [Code.add_default_eqn_attrib] else [];
 
       val anonymous_notes =
-        [(rel_eq_thms, code_attrs @ nitpicksimp_attrs)]
+        [(rel_code_thms, code_attrs @ nitpicksimp_attrs)]
         |> map (fn (thms, attrs) => ((Binding.empty, attrs), [(thms, [])]));
 
       val notes =
         [(case_transferN, [case_transfer_thm], K []),
          (ctr_transferN, ctr_transfer_thms, K []),

 
       val (noted, lthy') =
         lthy
         |> Spec_Rules.add Spec_Rules.Equational (`(single o lhs_head_of o hd) map_thms)
         |> fp = Least_FP
-          ? Spec_Rules.add Spec_Rules.Equational (`(single o lhs_head_of o hd) rel_eq_thms)
+          ? Spec_Rules.add Spec_Rules.Equational (`(single o lhs_head_of o hd) rel_code_thms)
         |> Spec_Rules.add Spec_Rules.Equational (`(single o lhs_head_of o hd) set0_thms)
         |> Local_Theory.notes (anonymous_notes @ notes);
 
       val subst = Morphism.thm (substitute_noted_thm noted);
     in