src/HOL/Tools/Lifting/lifting_setup.ML

 fun define_abs_type gen_code quot_thm lthy =
   if gen_code andalso Lifting_Def.can_generate_code_cert quot_thm then
     let
       val abs_type_thm = quot_thm RS @{thm Quotient_abs_rep}
       val add_abstype_attribute = 
-          Thm.declaration_attribute (fn thm => Context.mapping (Code.add_abstype thm) I)
+          Thm.declaration_attribute (fn thm => Context.mapping (Code.add_abstype_default thm) I)
         val add_abstype_attrib = Attrib.internal (K add_abstype_attribute)
     in
       lthy
         |> (snd oo Local_Theory.note) ((Binding.empty, [add_abstype_attrib]), [abs_type_thm])
     end