src/Pure/Isar/rule_cases.ML

       | SOME names => map (fn name => (name, get_case_concls th name)) names);
     val cases_hyps =
       (case lookup_cases_hyp_names th of
         NONE => replicate (length cases) []
       | SOME names => names);
-    fun regroup ((name,concls),hyps) = ((name,hyps),concls)
-  in (map regroup (cases ~~ cases_hyps), n) end;
+    fun regroup (name, concls) hyps = ((name, hyps), concls);
+  in (map2 regroup cases cases_hyps, n) end;
 
 
 (* params *)
 
 fun rename_params xss th =