src/HOL/Tools/record.ML

       val ensure_exhaustive_record =
         ensure_sort_record (@{sort full_exhaustive}, mk_full_exhaustive_eq);
     in
       thy
       |> Code.add_datatype [ext]
-      |> fold Code.add_default_eqn simps
+      |> fold (Code.add_eqn (Code.Equation, true)) simps
       |> Class.instantiation ([ext_tyco], vs, [HOLogic.class_equal])
       |> `(fn lthy => Syntax.check_term lthy eq)
       |-> (fn eq => Specification.definition NONE [] [] (Attrib.empty_binding, eq))
       |-> (fn (_, (_, eq_def)) =>
          Class.prove_instantiation_exit_result Morphism.thm tac eq_def)
       |-> (fn eq_def => fn thy =>
             thy
             |> Code.del_eqn eq_def
-            |> Code.add_default_eqn (mk_eq (Proof_Context.init_global thy) eq_def))
-      |> (fn thy => Code.add_nbe_default_eqn (mk_eq_refl (Proof_Context.init_global thy)) thy)
+            |> Code.add_eqn (Code.Equation, true) (mk_eq (Proof_Context.init_global thy) eq_def))
+      |> (fn thy => Code.add_eqn (Code.Nbe, true) (mk_eq_refl (Proof_Context.init_global thy)) thy)
       |> ensure_random_record ext_tyco vs (fst ext) (binder_types (snd ext))
       |> ensure_exhaustive_record ext_tyco vs (fst ext) (binder_types (snd ext))
     end
   else thy;
 

           |> (Global_Theory.add_defs false o
                 map (Thm.no_attributes o apfst (Binding.concealed o Binding.name))) sel_specs
           ||>> (Global_Theory.add_defs false o
                 map (Thm.no_attributes o apfst (Binding.concealed o Binding.name))) upd_specs
           ||>> (Global_Theory.add_defs false o
-                map (rpair [Code.add_default_eqn_attribute]
+                map (rpair [Code.add_default_eqn_attribute Code.Equation]
                 o apfst (Binding.concealed o Binding.name)))
             [make_spec, fields_spec, extend_spec, truncate_spec]);
     val defs_ctxt = Proof_Context.init_global defs_thy;
 
     (* prepare propositions *)