# HG changeset patch
# User wenzelm
# Date 1435227209 -7200
# Node ID 380d5a433719f277f6bb0c0401cace43728d6c59
# Parent  e549969355b2bb4e1360299fb7bdb5078102ff3a
tuned;

diff -r e549969355b2 -r 380d5a433719 src/Pure/Isar/rule_cases.ML
--- a/src/Pure/Isar/rule_cases.ML	Thu Jun 25 12:10:07 2015 +0200
+++ b/src/Pure/Isar/rule_cases.ML	Thu Jun 25 12:13:29 2015 +0200
@@ -424,8 +424,8 @@
       (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 *)