Adapted to changes in cases method.

--- a/src/HOL/Bali/DeclConcepts.thy	Sat Jan 30 17:01:01 2010 +0100
+++ b/src/HOL/Bali/DeclConcepts.thy	Sat Jan 30 17:03:46 2010 +0100
@@ -915,23 +915,15 @@
     assume "G \<turnstile> m member_of C"
     then show "n=m"
     proof (cases)
-      case (Immediate m' _)
-      with eqid 
-      have "m=m'"
-           "memberid n = memberid m" 
-           "G\<turnstile> mbr m declared_in C" 
-           "declclass m = C"
-        by auto
-      with member_n   
+      case Immediate
+      with eqid member_n
       show ?thesis
         by (cases n, cases m) 
            (auto simp add: declared_in_def 
                            cdeclaredmethd_def cdeclaredfield_def
                     split: memberdecl.splits)
     next
-      case (Inherited m' _ _)
-      then have "G\<turnstile> memberid m undeclared_in C"
-        by simp
+      case Inherited
       with eqid member_n
       show ?thesis
         by (cases n) (auto dest: declared_not_undeclared)
@@ -1656,10 +1648,7 @@
     from member_of
     show "?Methd C"
     proof (cases)
-      case (Immediate membr Ca)
-      then have "Ca=C" "membr = method sig m" and 
-                "G\<turnstile>Methd sig m declared_in C" "declclass m = C"
-        by (cases m,auto)
+      case Immediate
       with clsC 
       have "table_of (map (\<lambda>(s, m). (s, C, m)) (methods c)) sig = Some m"
         by (cases m)
@@ -1669,13 +1658,12 @@
       show ?thesis
         by (simp add: methd_rec)
     next
-      case (Inherited membr Ca S)
+      case (Inherited S)
       with clsC
-      have eq_Ca_C: "Ca=C" and
-            undecl: "G\<turnstile>mid sig undeclared_in C" and
+      have  undecl: "G\<turnstile>mid sig undeclared_in C" and
              super: "G \<turnstile>Methd sig m member_of (super c)"
         by (auto dest: subcls1D)
-      from eq_Ca_C clsC undecl 
+      from clsC undecl 
       have "table_of (map (\<lambda>(s, m). (s, C, m)) (methods c)) sig = None"
         by (auto simp add: undeclared_in_def cdeclaredmethd_def
                     intro: table_of_mapconst_NoneI)

--- a/src/HOL/IMP/Transition.thy	Sat Jan 30 17:01:01 2010 +0100
+++ b/src/HOL/IMP/Transition.thy	Sat Jan 30 17:03:46 2010 +0100
@@ -205,20 +205,16 @@
     (is "\<exists>i j s'. ?Q i j s'")
   proof (cases set: evalc1)
     case Semi1
-    then obtain s' where
-        "co = Some c2" and "s''' = s'" and "\<langle>c1, s\<rangle> \<longrightarrow>\<^sub>1 \<langle>s'\<rangle>"
-      by auto
-    with 1 n have "?Q 1 n s'" by simp
+    from `co = Some c2` and `\<langle>c1, s\<rangle> \<longrightarrow>\<^sub>1 \<langle>s'''\<rangle>` and 1 n
+    have "?Q 1 n s'''" by simp
     thus ?thesis by blast
   next
-    case Semi2
-    then obtain c1' s' where
-        "co = Some (c1'; c2)" "s''' = s'" and
-        c1: "\<langle>c1, s\<rangle> \<longrightarrow>\<^sub>1 \<langle>c1', s'\<rangle>"
-      by auto
-    with n have "\<langle>c1'; c2, s'\<rangle> -n\<rightarrow>\<^sub>1 \<langle>s''\<rangle>" by simp
+    case (Semi2 c1')
+    note c1 = `\<langle>c1, s\<rangle> \<longrightarrow>\<^sub>1 \<langle>c1', s'''\<rangle>`
+    with `co = Some (c1'; c2)` and n
+    have "\<langle>c1'; c2, s'''\<rangle> -n\<rightarrow>\<^sub>1 \<langle>s''\<rangle>" by simp
     with Suc.hyps obtain i j s0 where
-        c1': "\<langle>c1',s'\<rangle> -i\<rightarrow>\<^sub>1 \<langle>s0\<rangle>" and
+        c1': "\<langle>c1',s'''\<rangle> -i\<rightarrow>\<^sub>1 \<langle>s0\<rangle>" and
         c2:  "\<langle>c2,s0\<rangle> -j\<rightarrow>\<^sub>1 \<langle>s''\<rangle>" and
         i:   "n = i+j"
       by fast
@@ -228,7 +224,7 @@
     with c2 i
     have "?Q (i+1) j s0" by simp
     thus ?thesis by blast
-  qed auto -- "the remaining cases cannot occur"
+  qed
 qed
 
 

--- a/src/HOL/Lambda/Eta.thy	Sat Jan 30 17:01:01 2010 +0100
+++ b/src/HOL/Lambda/Eta.thy	Sat Jan 30 17:03:46 2010 +0100
@@ -273,13 +273,13 @@
       by (rule eta_case)
     with eta show ?thesis by simp
   next
-    case (abs r u)
-    hence "r \<rightarrow>\<^sub>\<eta> s'" by simp
-    then obtain t' where r: "r => t'" and t': "t' \<rightarrow>\<^sub>\<eta>\<^sup>* t" by (iprover dest: abs')
+    case (abs r)
+    from `r \<rightarrow>\<^sub>\<eta> s'`
+    obtain t' where r: "r => t'" and t': "t' \<rightarrow>\<^sub>\<eta>\<^sup>* t" by (iprover dest: abs')
     from r have "Abs r => Abs t'" ..
     moreover from t' have "Abs t' \<rightarrow>\<^sub>\<eta>\<^sup>* Abs t" by (rule rtrancl_eta_Abs)
     ultimately show ?thesis using abs by simp iprover
-  qed simp_all
+  qed
 next
   case (app u u' t t')
   from `s \<rightarrow>\<^sub>\<eta> u \<degree> t` show ?case
@@ -291,20 +291,20 @@
       by (rule eta_case)
     with eta show ?thesis by simp
   next
-    case (appL s' t'' u'')
-    hence "s' \<rightarrow>\<^sub>\<eta> u" by simp
-    then obtain r where s': "s' => r" and r: "r \<rightarrow>\<^sub>\<eta>\<^sup>* u'" by (iprover dest: app)
+    case (appL s')
+    from `s' \<rightarrow>\<^sub>\<eta> u`
+    obtain r where s': "s' => r" and r: "r \<rightarrow>\<^sub>\<eta>\<^sup>* u'" by (iprover dest: app)
     from s' and app have "s' \<degree> t => r \<degree> t'" by simp
     moreover from r have "r \<degree> t' \<rightarrow>\<^sub>\<eta>\<^sup>* u' \<degree> t'" by (simp add: rtrancl_eta_AppL)
     ultimately show ?thesis using appL by simp iprover
   next
-    case (appR s' t'' u'')
-    hence "s' \<rightarrow>\<^sub>\<eta> t" by simp
-    then obtain r where s': "s' => r" and r: "r \<rightarrow>\<^sub>\<eta>\<^sup>* t'" by (iprover dest: app)
+    case (appR s')
+    from `s' \<rightarrow>\<^sub>\<eta> t`
+    obtain r where s': "s' => r" and r: "r \<rightarrow>\<^sub>\<eta>\<^sup>* t'" by (iprover dest: app)
     from s' and app have "u \<degree> s' => u' \<degree> r" by simp
     moreover from r have "u' \<degree> r \<rightarrow>\<^sub>\<eta>\<^sup>* u' \<degree> t'" by (simp add: rtrancl_eta_AppR)
     ultimately show ?thesis using appR by simp iprover
-  qed simp
+  qed
 next
   case (beta u u' t t')
   from `s \<rightarrow>\<^sub>\<eta> Abs u \<degree> t` show ?case
@@ -316,9 +316,8 @@
       by (rule eta_case)
     with eta show ?thesis by simp
   next
-    case (appL s' t'' u'')
-    hence "s' \<rightarrow>\<^sub>\<eta> Abs u" by simp
-    thus ?thesis
+    case (appL s')
+    from `s' \<rightarrow>\<^sub>\<eta> Abs u` show ?thesis
     proof cases
       case (eta s'' dummy)
       have "Abs (lift u 1) = lift (Abs u) 0" by simp
@@ -332,23 +331,23 @@
       with s have "s => u'[t'/0]" by simp
       thus ?thesis by iprover
     next
-      case (abs r r')
-      hence "r \<rightarrow>\<^sub>\<eta> u" by simp
-      then obtain r'' where r: "r => r''" and r'': "r'' \<rightarrow>\<^sub>\<eta>\<^sup>* u'" by (iprover dest: beta)
+      case (abs r)
+      from `r \<rightarrow>\<^sub>\<eta> u`
+      obtain r'' where r: "r => r''" and r'': "r'' \<rightarrow>\<^sub>\<eta>\<^sup>* u'" by (iprover dest: beta)
       from r and beta have "Abs r \<degree> t => r''[t'/0]" by simp
       moreover from r'' have "r''[t'/0] \<rightarrow>\<^sub>\<eta>\<^sup>* u'[t'/0]"
         by (rule rtrancl_eta_subst')
       ultimately show ?thesis using abs and appL by simp iprover
-    qed simp_all
+    qed
   next
-    case (appR s' t'' u'')
-    hence "s' \<rightarrow>\<^sub>\<eta> t" by simp
-    then obtain r where s': "s' => r" and r: "r \<rightarrow>\<^sub>\<eta>\<^sup>* t'" by (iprover dest: beta)
+    case (appR s')
+    from `s' \<rightarrow>\<^sub>\<eta> t`
+    obtain r where s': "s' => r" and r: "r \<rightarrow>\<^sub>\<eta>\<^sup>* t'" by (iprover dest: beta)
     from s' and beta have "Abs u \<degree> s' => u'[r/0]" by simp
     moreover from r have "u'[r/0] \<rightarrow>\<^sub>\<eta>\<^sup>* u'[t'/0]"
       by (rule rtrancl_eta_subst'')
     ultimately show ?thesis using appR by simp iprover
-  qed simp
+  qed
 qed
 
 theorem eta_postponement':

--- a/src/HOL/Nominal/Examples/Pattern.thy	Sat Jan 30 17:01:01 2010 +0100
+++ b/src/HOL/Nominal/Examples/Pattern.thy	Sat Jan 30 17:03:46 2010 +0100
@@ -575,13 +575,13 @@
   and R: "\<And>U. S = T \<rightarrow> U \<Longrightarrow> (x, T) # \<Gamma> \<turnstile> t : U \<Longrightarrow> P"
   shows P using ty
 proof cases
-  case (Abs x' T' \<Gamma>' t' U)
+  case (Abs x' T' t' U)
   obtain y::name where y: "y \<sharp> (x, \<Gamma>, \<lambda>x':T'. t')"
     by (rule exists_fresh) (auto intro: fin_supp)
   from `(\<lambda>x:T. t) = (\<lambda>x':T'. t')` [symmetric]
   have x: "x \<sharp> (\<lambda>x':T'. t')" by (simp add: abs_fresh)
   have x': "x' \<sharp> (\<lambda>x':T'. t')" by (simp add: abs_fresh)
-  from `(x', T') # \<Gamma>' \<turnstile> t' : U` have x'': "x' \<sharp> \<Gamma>'"
+  from `(x', T') # \<Gamma> \<turnstile> t' : U` have x'': "x' \<sharp> \<Gamma>"
     by (auto dest: valid_typing)
   have "(\<lambda>x:T. t) = (\<lambda>x':T'. t')" by fact
   also from x x' y have "\<dots> = [(x, y)] \<bullet> [(x', y)] \<bullet> (\<lambda>x':T'. t')"
@@ -592,10 +592,10 @@
   then have T: "T = T'" and t: "[(x, y)] \<bullet> [(x', y)] \<bullet> t' = t"
     by (simp_all add: trm.inject alpha)
   from Abs T have "S = T \<rightarrow> U" by simp
-  moreover from `(x', T') # \<Gamma>' \<turnstile> t' : U`
-  have "[(x, y)] \<bullet> [(x', y)] \<bullet> ((x', T') # \<Gamma>' \<turnstile> t' : U)"
+  moreover from `(x', T') # \<Gamma> \<turnstile> t' : U`
+  have "[(x, y)] \<bullet> [(x', y)] \<bullet> ((x', T') # \<Gamma> \<turnstile> t' : U)"
     by (simp add: perm_bool)
-  with T t y `\<Gamma> = \<Gamma>'` x'' fresh have "(x, T) # \<Gamma> \<turnstile> t : U"
+  with T t y x'' fresh have "(x, T) # \<Gamma> \<turnstile> t : U"
     by (simp add: eqvts swap_simps perm_fresh_fresh fresh_prod)
   ultimately show ?thesis by (rule R)
 qed simp_all
@@ -764,7 +764,7 @@
   and R: "\<And>T \<Delta>. \<Gamma> \<turnstile> t : T \<Longrightarrow> \<turnstile> p : T \<Rightarrow> \<Delta> \<Longrightarrow> \<Delta> @ \<Gamma> \<turnstile> u : U \<Longrightarrow> P"
   shows P using ty
 proof cases
-  case (Let p' t' \<Gamma>' T \<Delta> u' U')
+  case (Let p' t' T \<Delta> u')
   then have "(supp \<Delta>::name set) \<sharp>* \<Gamma>"
     by (auto intro: valid_typing valid_app_freshs)
   with Let have "(supp p'::name set) \<sharp>* \<Gamma>"
@@ -776,7 +776,7 @@
   moreover from Let have "pat_type p = pat_type p'"
     by (simp add: trm.inject)
   moreover note distinct
-  moreover from `\<Delta> @ \<Gamma>' \<turnstile> u' : U'` have "valid (\<Delta> @ \<Gamma>')"
+  moreover from `\<Delta> @ \<Gamma> \<turnstile> u' : U` have "valid (\<Delta> @ \<Gamma>)"
     by (rule valid_typing)
   then have "valid \<Delta>" by (rule valid_appD)
   with `\<turnstile> p' : T \<Rightarrow> \<Delta>` have "distinct (pat_vars p')"