diff -r e344dc82f6c2 -r 4eaf35781b23 src/HOL/Tools/Quickcheck/random_generators.ML
--- a/src/HOL/Tools/Quickcheck/random_generators.ML	Wed Jun 22 16:04:03 2016 +0200
+++ b/src/HOL/Tools/Quickcheck/random_generators.ML	Thu Jun 23 11:01:14 2016 +0200
@@ -141,7 +141,7 @@
         val proj_eqs = map2 (fn v => fn proj => (v, lambda arg proj)) vs projs;
         val proj_defs = map2 (fn Free (name, _) => fn (_, rhs) =>
           ((Binding.concealed (Binding.name name), NoSyn),
-            (apfst Binding.concealed Attrib.empty_binding, rhs))) vs proj_eqs;
+            (apfst Binding.concealed Binding.empty_atts, rhs))) vs proj_eqs;
         val aux_eq' = Pattern.rewrite_term thy proj_eqs [] aux_eq;
         fun prove_eqs aux_simp proj_defs lthy = 
           let