src/HOL/Tools/Datatype/datatype_codegen.ML

       |> Logic.dest_equals
       |> fst
       |> Term.strip_comb
       |> apsnd (fst o split_last)
       |> list_comb;
-    val lhs = Free (Name.variant params "case", Term.fastype_of rhs);
+    val lhs = Free (singleton (Name.variant_list params) "case", Term.fastype_of rhs);
     val asm = (Thm.cterm_of thy o Logic.mk_equals) (lhs, rhs);
   in
     thms
     |> Conjunction.intr_balanced
     |> Raw_Simplifier.rewrite_rule [(Thm.symmetric o Thm.assume) asm]