src/HOL/Tools/Lifting/lifting_def_code_dt.ML

   var qty rhs tac par_thms lthy
 
 
 (** from parsed parameters to the config record **)
 
-fun map_config_code_dt f1 f2 { code_dt = code_dt, lift_config = lift_config } =
-  { code_dt = f1 code_dt, lift_config = f2 lift_config }
+fun map_config_code_dt f1 f2 ({code_dt = code_dt, lift_config = lift_config}: config_code_dt) =
+  {code_dt = f1 code_dt, lift_config = f2 lift_config}
 
 fun update_config_code_dt nval = map_config_code_dt (K nval) I
 
 val config_flags = [("code_dt", update_config_code_dt true)]