adapted variable order for inductive cases (determined by read_specification *before* expanding abbreviations);

--- a/src/HOL/Bali/AxSound.thy	Wed Sep 26 19:18:01 2007 +0200
+++ b/src/HOL/Bali/AxSound.thy	Wed Sep 26 19:19:38 2007 +0200
@@ -2017,7 +2017,7 @@
                 \<rbrakk>\<Longrightarrow> (P'\<leftarrow>=False\<down>=\<diamondsuit>) v s' Z"
 	  (is "PROP ?Hyp n t s v s'")
 	proof (induct)
-	  case (Loop s0' e' n' b s1' c' s2' l' s3' Y' T E)
+	  case (Loop s0' e' b n' s1' c' s2' l' s3' Y' T E)
 	  note while = `(\<langle>l'\<bullet> While(e') c'\<rangle>\<^sub>s::term) = \<langle>l\<bullet> While(e) c\<rangle>\<^sub>s`
           hence eqs: "l'=l" "e'=e" "c'=c" by simp_all
 	  note valid_A = `\<forall>t\<in>A. G\<Turnstile>n'\<Colon>t`

--- a/src/HOL/Bali/Evaln.thy	Wed Sep 26 19:18:01 2007 +0200
+++ b/src/HOL/Bali/Evaln.thy	Wed Sep 26 19:19:38 2007 +0200
@@ -410,7 +410,7 @@
   shows "G\<turnstile>s0 \<midarrow>t\<succ>\<rightarrow> (v,s1)"
 using evaln 
 proof (induct)
-  case (Loop s0 e n b s1 c s2 l s3)
+  case (Loop s0 e b n s1 c s2 l s3)
   note `G\<turnstile>Norm s0 \<midarrow>e-\<succ>b\<rightarrow> s1`
   moreover
   have "if the_Bool b