--- a/Nominal/Nominal2.thy	Wed Dec 22 09:13:25 2010 +0000
+++ b/Nominal/Nominal2.thy	Wed Dec 22 10:32:01 2010 +0000
@@ -296,18 +296,17 @@
       |> split_list
       |>> (map o map) strip_params_prems_concl     
 
-    val prems = map2 (process_ecase lthy'' c) (flat ecases) (flat bclausesss)
+    val premss = ((map2 o map2) (process_ecase lthy'' c) ecases bclausesss)
+
   in
-    Goal.prove_multi lthy'' [] prems main_concls
-     (fn {prems:thm list, context} =>
-        let
-           val prems' = partitions prems (map length bclausesss)
-        in
-          EVERY1 [Goal.conjunction_tac,
-            RANGE (map2 (case_tac context c bn_finite_thms eq_iff_thms bn_eqvt permute_bns perm_bn_alphas) 
-                      (prems' ~~ bclausesss) exhausts')]
-        end)
-    |> ProofContext.export lthy'' lthy
+    map2 (fn (prems, bclausess) => fn (exh, concl) =>
+      Goal.prove lthy'' [] prems concl 
+       (fn {prems: thm list, context} =>
+          HEADGOAL (case_tac context c bn_finite_thms eq_iff_thms bn_eqvt permute_bns perm_bn_alphas 
+            (prems, bclausess) exh)
+       )
+    ) (premss ~~ bclausesss) (exhausts' ~~ main_concls)
+   |> ProofContext.export lthy'' lthy
   end
 *}