adopting proofs due to new list comprehension to set comprehension simproc

--- a/src/HOL/Decision_Procs/MIR.thy	Fri Jan 07 18:10:35 2011 +0100
+++ b/src/HOL/Decision_Procs/MIR.thy	Fri Jan 07 18:10:42 2011 +0100
@@ -3585,9 +3585,9 @@
     thus "(UNION M (\<lambda> (a,b,c). set (f (a,b,c)))) = (UNION M (\<lambda> (a,b,c). set (g a b c)))"
       by (auto simp add: split_def)
   qed
-  have "?SS (Floor a) = UNION (?SS a) (\<lambda>x. set (?ff x))" 
-    by (auto simp add: foldl_conv_concat)
-  also have "\<dots> = UNION (?SS a) (\<lambda> (p,n,s). set (?ff (p,n,s)))" by auto
+  have "?SS (Floor a) = UNION (?SS a) (\<lambda>x. set (?ff x))"
+    by (auto simp add: foldl_conv_concat simp del: iupt.simps)
+  also have "\<dots> = UNION (?SS a) (\<lambda> (p,n,s). set (?ff (p,n,s)))" by blast
   also have "\<dots> = 
     ((UNION {(p,n,s). (p,n,s) \<in> ?SS a \<and> n=0} (\<lambda> (p,n,s). set (?ff (p,n,s)))) Un 
     (UNION {(p,n,s). (p,n,s) \<in> ?SS a \<and> n>0} (\<lambda> (p,n,s). set (?ff (p,n,s)))) Un 
@@ -3743,8 +3743,8 @@
       by (auto simp add: split_def)
   qed
 
-  have "?SS (Floor a) = UNION (?SS a) (\<lambda>x. set (?ff x))" by (auto simp add: foldl_conv_concat) 
-  also have "\<dots> = UNION (?SS a) (\<lambda> (p,n,s). set (?ff (p,n,s)))" by auto
+  have "?SS (Floor a) = UNION (?SS a) (\<lambda>x. set (?ff x))" by (auto simp add: foldl_conv_concat simp del: iupt.simps) 
+  also have "\<dots> = UNION (?SS a) (\<lambda> (p,n,s). set (?ff (p,n,s)))" by blast
   also have "\<dots> = 
     ((UNION {(p,n,s). (p,n,s) \<in> ?SS a \<and> n=0} (\<lambda> (p,n,s). set (?ff (p,n,s)))) Un 
     (UNION {(p,n,s). (p,n,s) \<in> ?SS a \<and> n>0} (\<lambda> (p,n,s). set (?ff (p,n,s)))) Un 

--- a/src/HOL/MicroJava/BV/Typing_Framework_JVM.thy	Fri Jan 07 18:10:35 2011 +0100
+++ b/src/HOL/MicroJava/BV/Typing_Framework_JVM.thy	Fri Jan 07 18:10:42 2011 +0100
@@ -89,14 +89,14 @@
   apply clarsimp
   apply (erule disjE)
    apply (fastsimp dest: field_fields fields_is_type)
-  apply (simp add: match_some_entry split: split_if_asm)
+  apply (simp add: match_some_entry image_iff)
   apply (rule_tac x=1 in exI)
   apply fastsimp
 
   apply clarsimp
   apply (erule disjE)
    apply fastsimp
-  apply (simp add: match_some_entry split: split_if_asm)
+  apply (simp add: match_some_entry image_iff)
   apply (rule_tac x=1 in exI)
   apply fastsimp