src/HOL/Tools/function_package/size.ML

     val SOME (_, _, constrs) = AList.lookup op = descr index
   in constrs end;
 
 val app = curry (list_comb o swap);
 
-fun prove_size_thms (info : datatype_info) new_type_names thy =
+fun prove_size_thms (info : info) new_type_names thy =
   let
     val {descr, alt_names, sorts, rec_names, rec_rewrites, induction, ...} = info;
     val l = length new_type_names;
     val alt_names' = (case alt_names of
       NONE => replicate l NONE | SOME names => map SOME names);