src/HOL/Bali/AxCompl.thy

     fix v e c es
     have "G,A\<turnstile>{=:n} \<langle>v\<rangle>\<^sub>v\<succ> {G\<rightarrow>}" and 
       "G,A\<turnstile>{=:n} \<langle>e\<rangle>\<^sub>e\<succ> {G\<rightarrow>}" and
       "G,A\<turnstile>{=:n} \<langle>c\<rangle>\<^sub>s\<succ> {G\<rightarrow>}" and  
       "G,A\<turnstile>{=:n} \<langle>es\<rangle>\<^sub>l\<succ> {G\<rightarrow>}"
-    proof (induct rule: var_expr_stmt.induct)
+    proof (induct rule: var_expr_stmt.inducts)
       case (LVar v)
       show "G,A\<turnstile>{=:n} \<langle>LVar v\<rangle>\<^sub>v\<succ> {G\<rightarrow>}"
 	apply (rule MGFn_NormalI)
 	apply (rule ax_derivs.LVar [THEN conseq1])
 	apply (clarsimp)