src/HOL/Tools/function_package/size.ML

   in
     SizeData.map (fold (Symtab.update_new o apsnd (rpair size_thms))
       (new_type_names ~~ size_names)) thy''
   end;
 
-fun add_size_thms (new_type_names as name :: _) thy =
+fun add_size_thms config (new_type_names as name :: _) thy =
   let
     val info as {descr, alt_names, ...} = DatatypePackage.the_datatype thy name;
     val prefix = Long_Name.map_base_name (K (space_implode "_"
       (the_default (map Long_Name.base_name new_type_names) alt_names))) name;
     val no_size = exists (fn (_, (_, _, constrs)) => exists (fn (_, cargs) => exists (fn dt =>