src/HOL/Tools/Quickcheck/quickcheck_common.ML

       val eqs_t = mk_equations (map2 (fn name => fn T => Free (name, T)) names Ts)
     in
       Function.add_function
         (map (fn (name, T) => (Binding.concealed (Binding.name name), SOME T, NoSyn))
           (names ~~ Ts))
-        (map (fn t => (((Binding.concealed Binding.empty, []), t), [])) eqs_t)
+        (map (fn t => (((Binding.concealed Binding.empty, []), t), [], [])) eqs_t)
         Function_Common.default_config pat_completeness_auto
       #> snd
       #> (fn lthy => Function.prove_termination NONE (the termination_tac lthy) lthy)
       #> snd
     end