--- a/Nominal/Nominal2.thy	Wed Dec 22 10:32:01 2010 +0000
+++ b/Nominal/Nominal2.thy	Wed Dec 22 12:17:49 2010 +0000
@@ -207,7 +207,7 @@
 
 ML {*
 fun case_tac ctxt c bn_finite_thms eq_iff_thms bn_eqvt permute_bns perm_bn_alphas 
-  (prems, bclausess) qexhaust_thm =
+  prems bclausess qexhaust_thm =
   let
     fun aux_tac prem bclauses =
       case (get_all_binders bclauses) of
@@ -276,13 +276,12 @@
             rtac side_thm 1 
           end) ctxt
   in
-    rtac qexhaust_thm THEN' RANGE (map2 aux_tac prems bclausess)
+    EVERY1 [rtac qexhaust_thm, RANGE (map2 aux_tac prems bclausess)]
   end
 *}
 
-
 ML {*
-fun prove_strong_exhausts lthy exhausts qtrms bclausesss bn_finite_thms eq_iff_thms bn_eqvt permute_bns 
+fun prove_strong_exhausts lthy exhausts bclausesss bn_finite_thms eq_iff_thms bn_eqvt permute_bns
   perm_bn_alphas =
   let
     val ((_, exhausts'), lthy') = Variable.import true exhausts lthy 
@@ -296,17 +295,17 @@
       |> split_list
       |>> (map o map) strip_params_prems_concl     
 
-    val premss = ((map2 o map2) (process_ecase lthy'' c) ecases bclausesss)
+    val premss = (map2 o map2) (process_ecase lthy'' c) ecases bclausesss
+   
+    fun tac bclausess exhaust {prems, context} =
+      case_tac context c bn_finite_thms eq_iff_thms bn_eqvt permute_bns perm_bn_alphas 
+        prems bclausess exhaust
 
+    fun prove prems bclausess exhaust concl =
+      Goal.prove lthy'' [] prems concl (tac bclausess exhaust)
   in
-    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
+    map4 prove premss bclausesss exhausts' main_concls
+    |> ProofContext.export lthy'' lthy
   end
 *}
 
@@ -824,7 +823,7 @@
     then prove_permute_bn_thms qtys qbns qperm_bns qinduct qperm_bn_simps qbn_defs qfv_qbn_eqvts lthyC
     else []
 
-  val qstrong_exhaust_thms = prove_strong_exhausts lthyC qexhausts qtrms bclauses qbn_finite_thms qeq_iffs'
+  val qstrong_exhaust_thms = prove_strong_exhausts lthyC qexhausts bclauses qbn_finite_thms qeq_iffs'
     qfv_qbn_eqvts qpermute_bn_thms qperm_bn_alpha_thms