--- 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
 
 

--- a/Nominal/nominal_library.ML	Wed Dec 22 10:32:01 2010 +0000
+++ b/Nominal/nominal_library.ML	Wed Dec 22 12:17:49 2010 +0000
@@ -9,8 +9,9 @@
   val last2: 'a list -> 'a * 'a
   val order: ('a * 'a -> bool) -> 'a list -> ('a * 'b) list -> 'b list
   val remove_dups: ('a * 'a -> bool) -> 'a list -> 'a list
-  val partitions: 'a list -> int list -> 'a list list
+  val map4: ('a -> 'b -> 'c -> 'd -> 'e) -> 'a list -> 'b list -> 'c list -> 'd list -> 'e list
   val split_filter: ('a -> bool) -> 'a list -> 'a list * 'a list
+  
 
   val is_true: term -> bool
  
@@ -138,14 +139,8 @@
   | last2 [x, y] = (x, y)
   | last2 (_ :: xs) = last2 xs
 
-(* partitions a set according to the numbers in the int list *)
-fun partitions [] [] = []
-  | partitions xs (i :: js) = 
-      let
-        val (head, tail) = chop i xs
-      in
-        head :: partitions tail js
-      end
+fun map4 _ [] [] [] [] = []
+  | map4 f (x :: xs) (y :: ys) (z :: zs) (u :: us) = f x y z u :: map4 f xs ys zs us
 
 fun split_filter f [] = ([], [])
   | split_filter f (x :: xs) =