--- a/src/HOL/Tools/Quickcheck/random_generators.ML Wed Apr 27 10:03:35 2016 +0200
+++ b/src/HOL/Tools/Quickcheck/random_generators.ML Thu Apr 28 09:43:11 2016 +0200
@@ -266,8 +266,8 @@
|> random_aux_specification prfx random_auxN auxs_eqs
|> `(fn lthy => map (Syntax.check_term lthy) random_defs)
|-> (fn random_defs' => fold_map (fn random_def =>
- Specification.definition (NONE, (apfst Binding.concealed
- Attrib.empty_binding, random_def))) random_defs')
+ Specification.definition NONE []
+ ((Binding.concealed Binding.empty, []), random_def)) random_defs')
|> snd
|> Class.prove_instantiation_exit (fn ctxt => Class.intro_classes_tac ctxt [])
end;