--- a/Nominal/Ex/Let.thy	Wed Dec 22 09:13:25 2010 +0000
+++ b/Nominal/Ex/Let.thy	Wed Dec 22 10:32:01 2010 +0000
@@ -30,39 +30,6 @@
 thm trm_assn.exhaust
 thm trm_assn.strong_exhaust
 
-lemma strong_exhaust1:
-  fixes c::"'a::fs"
-  assumes "\<And>name. y = Var name \<Longrightarrow> P" 
-  and     "\<And>trm1 trm2. y = App trm1 trm2 \<Longrightarrow> P"
-  and     "\<And>name trm. \<lbrakk>{atom name} \<sharp>* c; y = Lam name trm\<rbrakk> \<Longrightarrow> P" 
-  and     "\<And>assn trm. \<lbrakk>set (bn assn) \<sharp>* c; y = Let assn trm\<rbrakk> \<Longrightarrow> P"
-  shows "P"
-apply(rule_tac y="y" in trm_assn.strong_exhaust(1))
-apply(rule assms(1))
-apply(assumption)
-apply(rule assms(2))
-apply(assumption)
-apply(rule assms(3))
-apply(assumption)
-apply(assumption)
-apply(rule assms(4))
-apply(assumption)
-apply(assumption)
-sorry
-
-
-lemma strong_exhaust2:
-  assumes "as = ANil \<Longrightarrow> P" 
-  and     "\<And>x t assn. \<lbrakk>as = ACons x t assn\<rbrakk> \<Longrightarrow> P" 
-  shows "P"
-apply(rule_tac y="as" in trm_assn.exhaust(2))
-apply(rule assms(1))
-apply(assumption)
-apply(rule assms(2))
-apply(assumption)+
-done
-
-
 lemma 
   fixes t::trm
   and   as::assn
@@ -76,12 +43,12 @@
   shows "P1 c t" "P2 c as"
 using assms
 apply(induction_schema)
-apply(rule_tac y="t" in strong_exhaust1)
+apply(rule_tac y="t" in trm_assn.strong_exhaust(1))
 apply(blast)
 apply(blast)
 apply(blast)
 apply(blast)
-apply(rule_tac as="as" in strong_exhaust2)
+apply(rule_tac ya="as" in trm_assn.strong_exhaust(2))
 apply(blast)
 apply(blast)
 apply(relation "measure (sum_case (\<lambda>y. size (snd y)) (\<lambda>z. size (snd z)))")

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

--- a/Nominal/ROOT.ML	Wed Dec 22 09:13:25 2010 +0000
+++ b/Nominal/ROOT.ML	Wed Dec 22 10:32:01 2010 +0000
@@ -24,6 +24,6 @@
     "Ex/TypeVarsTest",
     (*"Ex/Foo1",
     "Ex/Foo2",*)
-    "Ex/CoreHaskell"
+    "Ex/CoreHaskell",
     "Ex/CoreHaskell2"
     ];