src/HOL/IMP/Natural.thy

 *}
 theorem com_det:
   assumes "\<langle>c,s\<rangle> \<longrightarrow>\<^sub>c t" and "\<langle>c,s\<rangle> \<longrightarrow>\<^sub>c u"
   shows "u = t"
   using prems
-proof (induct fixing: u set: evalc)
+proof (induct arbitrary: u set: evalc)
   fix s u assume "\<langle>\<SKIP>,s\<rangle> \<longrightarrow>\<^sub>c u"
   thus "u = s" by simp
 next
   fix a s x u assume "\<langle>x :== a,s\<rangle> \<longrightarrow>\<^sub>c u"
   thus "u = s[x \<mapsto> a s]" by simp

 *}
 theorem
   assumes "\<langle>c,s\<rangle> \<longrightarrow>\<^sub>c t" and "\<langle>c,s\<rangle> \<longrightarrow>\<^sub>c u"
   shows "u = t"
   using prems
-proof (induct fixing: u)
+proof (induct arbitrary: u)
   -- "the simple @{text \<SKIP>} case for demonstration:"
   fix s u assume "\<langle>\<SKIP>,s\<rangle> \<longrightarrow>\<^sub>c u"
   thus "u = s" by simp
 next
   -- "and the only really interesting case, @{text \<WHILE>}:"