--- 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