src/HOL/Tools/Old_Datatype/old_rep_datatype.ML

       ([((prfx (Binding.name "simps"), []), [(simps, [])]),
         ((prfx (Binding.name "inducts"), []), [(inducts, [])]),
         ((prfx (Binding.name "splits"), []), [(maps (fn (x, y) => [x, y]) splits, [])]),
         ((Binding.empty, [Simplifier.simp_add]),
           [(flat case_rewrites @ flat distinct @ rec_rewrites, [])]),
-        ((Binding.empty, [Code.add_default_eqn_attribute Code.Equation]), [(rec_rewrites, [])]),
         ((Binding.empty, [iff_add]), [(flat inject, [])]),
         ((Binding.empty, [Classical.safe_elim NONE]),
           [(map (fn th => th RS notE) (flat distinct), [])]),
         ((Binding.empty, [Simplifier.cong_add]), [(case_cong_weaks, [])]),
         ((Binding.empty, [Induct.induct_simp_add]), [(flat (distinct @ inject), [])])] @
           named_rules @ unnamed_rules)
     |> snd
+    |> Code.declare_default_eqns_global (map (rpair true) rec_rewrites)
     |> Old_Datatype_Data.register dt_infos
     |> Context.theory_map (fold2 Case_Translation.register case_combs constrss)
     |> Old_Datatype_Data.interpretation_data (config, dt_names)
     |> pair dt_names
   end;