Adapted to new parse translation for case expressions.

--- a/src/HOL/Library/Coinductive_List.thy	Tue Apr 24 15:14:31 2007 +0200
+++ b/src/HOL/Library/Coinductive_List.thy	Tue Apr 24 15:15:52 2007 +0200
@@ -107,7 +107,7 @@
     next
       case (Some p)
       then have "LList_corec x f = CONS (fst p) (LList_corec (snd p) f)"
-        by (simp add: split_def LList_corec)
+        by (simp add: LList_corec split: prod.split)
       with L have ?CONS by auto
       then show ?thesis ..
     qed
@@ -244,7 +244,7 @@
       case (Some p)
       then have "?corec x =
           CONS (Datatype.Leaf (fst p)) (?corec (snd p))"
-        by (simp add: split_def LList_corec)
+        by (simp add: LList_corec split: prod.split)
       with L have ?CONS by auto
       then show ?thesis ..
     qed
@@ -271,12 +271,12 @@
     by (simp only: llist_corec_def)
   also from Some have "?rep_corec a =
       CONS (Datatype.Leaf (fst p)) (?rep_corec (snd p))"
-    by (simp add: split_def LList_corec)
+    by (simp add: LList_corec split: prod.split)
   also have "?rep_corec (snd p) = Rep_llist (?corec (snd p))"
     by (simp only: llist_corec_def Abs_llist_inverse LList_corec_type2)
   finally have "?corec a = LCons (fst p) (?corec (snd p))"
     by (simp only: LCons_def)
-  with Some show ?thesis by (simp add: split_def)
+  with Some show ?thesis by (simp split: prod.split)
 qed
 
 
@@ -457,7 +457,7 @@
       case (Some p)
       with h h' q have "q =
           (CONS (fst p) (h (snd p)), CONS (fst p) (h' (snd p)))"
-        by (simp add: split_def)
+        by (simp split: prod.split)
       then have ?EqCONS by (auto iff: diag_iff)
       then show ?thesis ..
     qed

--- a/src/HOL/MicroJava/Comp/CorrCompTp.thy	Tue Apr 24 15:14:31 2007 +0200
+++ b/src/HOL/MicroJava/Comp/CorrCompTp.thy	Tue Apr 24 15:15:52 2007 +0200
@@ -981,13 +981,13 @@
   \<Longrightarrow> bc_mt_corresp bc f sttp cG rT mxr 0"
 apply (simp add: bc_mt_corresp_def start_sttp_resp_def split_beta)
 apply (erule disjE)
-apply (simp add: max_ssize_def max_of_list_def ssize_sto_def split_beta)
+apply (simp add: max_ssize_def max_of_list_def ssize_sto_def split: prod.split)
 apply (intro strip)
 apply (simp add: start_sttp_resp_cons_def split_beta)
 apply (drule_tac x=sttp in spec, erule exE)
 apply simp
 apply (rule check_type_mono, assumption)
-apply (simp add: max_ssize_def max_of_list_def ssize_sto_def max_def split_beta)
+apply (simp add: max_ssize_def max_of_list_def ssize_sto_def max_def split: prod.split)
 done
 
   (* ********************************************************************** *)