src/HOL/Nominal/nominal_datatype.ML

         in
           ((Attrib.empty_binding, HOLogic.mk_Trueprop (HOLogic.mk_eq
             (Free (nth perm_names_types' i) $
                Free ("pi", mk_permT (TFree ("'x", @{sort type}))) $
                list_comb (c, args),
-             list_comb (c, map perm_arg (dts ~~ args))))), [])
+             list_comb (c, map perm_arg (dts ~~ args))))), [], [])
         end) constrs
       end) descr;
 
     val (perm_simps, thy2) =
       BNF_LFP_Compat.primrec_overloaded