src/HOL/Nominal/nominal_datatype.ML

--- a/src/HOL/Nominal/nominal_datatype.ML	Thu Apr 09 20:42:38 2015 +0200
+++ b/src/HOL/Nominal/nominal_datatype.ML	Thu Apr 09 22:53:26 2015 +0200
@@ -162,7 +162,7 @@
 fun fresh_star_const T U =
   Const (@{const_name Nominal.fresh_star}, HOLogic.mk_setT T --> U --> HOLogic.boolT);
 
-fun gen_nominal_datatype prep_specs config dts thy =
+fun gen_nominal_datatype prep_specs (config: Old_Datatype_Aux.config) dts thy =
   let
     val new_type_names = map (fn ((tname, _, _), _) => Binding.name_of tname) dts;