src/HOL/Tools/Quickcheck/random_generators.ML

     thy
     |> Class.instantiation (tycos, vs, @{sort random})
     |> 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 []
+          Specification.definition NONE [] []
             ((Binding.concealed Binding.empty, []), random_def)) random_defs')
     |> snd
     |> Class.prove_instantiation_exit (fn ctxt => Class.intro_classes_tac ctxt [])
   end;