--- a/src/Pure/Isar/code.ML Sat Nov 30 23:30:36 2024 +0100
+++ b/src/Pure/Isar/code.ML Sun Dec 01 14:01:47 2024 +0100
@@ -1465,8 +1465,7 @@
fun case_cong thy case_const (num_args, (pos, _)) =
let
- val ([x, y], ctxt) = fold_map Name.variant ["A", "A'"] Name.context;
- val (zs, _) = fold_map Name.variant (replicate (num_args - 1) "") ctxt;
+ val x :: y :: zs = Name.variants Name.context ("A" :: "A'" :: replicate (num_args - 1) "");
val (ws, vs) = chop pos zs;
val T = devarify (const_typ thy case_const);
val Ts = binder_types T;