src/HOL/Tools/Datatype/datatype_codegen.ML

      (case Datatype.info_of_case thy s of
         SOME {index, descr, ...} =>
           if is_some (get_assoc_code thy (s, T)) then NONE else
           SOME (pretty_case thy defs dep module brack
             (#3 (the (AList.lookup op = descr index))) c ts gr )
-      | NONE => case (Datatype.info_of_constr thy s, strip_type T) of
+      | NONE => case (Datatype.info_of_constr thy (s, T), strip_type T) of
         (SOME {index, descr, ...}, (_, U as Type (tyname, _))) =>
           if is_some (get_assoc_code thy (s, T)) then NONE else
           let
             val SOME (tyname', _, constrs) = AList.lookup op = descr index;
             val SOME args = AList.lookup op = constrs s