src/HOL/Tools/Quickcheck/quickcheck_common.ML

       #> snd
     end
   else
     fold_map (fn (name, T) => Local_Theory.define
         ((Binding.concealed (Binding.name name), NoSyn),
-          (apfst Binding.concealed Attrib.empty_binding, mk_undefined T))
+          (apfst Binding.concealed Binding.empty_atts, mk_undefined T))
       #> apfst fst) (names ~~ Ts)
     #> (fn (consts, lthy) =>
       let
         val eqs_t = mk_equations consts
         val eqs = map (fn eq => Goal.prove lthy argnames [] eq