diff -r bf4188deabb2 -r b13e5c3497f5 src/HOL/Bali/DefiniteAssignmentCorrect.thy
--- a/src/HOL/Bali/DefiniteAssignmentCorrect.thy	Tue Sep 09 20:51:36 2014 +0200
+++ b/src/HOL/Bali/DefiniteAssignmentCorrect.thy	Tue Sep 09 20:51:36 2014 +0200
@@ -102,8 +102,7 @@
 proof -
     have True and True and 
        "\<And> jmps' jmps. \<lbrakk>jumpNestingOkS jmps' c; jmps' \<subseteq> jmps\<rbrakk> \<Longrightarrow> jumpNestingOkS jmps c" 
-       and True
-  proof (induct rule: var_expr_stmt.inducts)
+  proof (induct rule: var.induct expr.induct stmt.induct)
     case (Lab j c jmps' jmps)
     note jmpOk = `jumpNestingOkS jmps' (j\<bullet> c)`
     note jmps = `jmps' \<subseteq> jmps`
@@ -2008,8 +2007,8 @@
   have  True and 
         "\<And> c v s0 s. \<lbrakk> constVal e = Some c; G\<turnstile>Norm s0 \<midarrow>e-\<succ>v\<rightarrow> s\<rbrakk> 
                       \<Longrightarrow> v = c \<and> normal s"
-        and True and True
-  proof (induct  rule: var_expr_stmt.inducts)
+        and True
+  proof (induct rule: var.induct expr.induct stmt.induct)
     case NewC hence False by simp thus ?case ..
   next
     case NewA hence False by simp thus ?case ..
@@ -2156,8 +2155,8 @@
   have True and 
        "\<And> c. \<lbrakk>constVal e = Some c;Env\<turnstile>e\<Colon>-PrimT Boolean\<rbrakk> 
                 \<Longrightarrow> typeof empty_dt c = Some (PrimT Boolean)"
-       and True and True 
-  proof (induct rule: var_expr_stmt.inducts)
+       and True 
+  proof (induct rule: var.induct expr.induct stmt.induct)
     case NewC hence False by simp thus ?case ..
   next
     case NewA hence False by simp thus ?case ..