--- a/src/HOL/Bali/AxSound.thy Sun Feb 16 21:33:28 2014 +0100
+++ b/src/HOL/Bali/AxSound.thy Sun Feb 16 21:33:28 2014 +0100
@@ -1543,10 +1543,10 @@
proof -
from normal_s2 conf_args
have "length vs = length pTs"
- by (simp add: list_all2_def)
+ by (simp add: list_all2_iff)
also from pTs_widen
have "\<dots> = length pTs'"
- by (simp add: widens_def list_all2_def)
+ by (simp add: widens_def list_all2_iff)
also from wf_dynM
have "\<dots> = length (pars (mthd dynM))"
by (simp add: wf_mdecl_def wf_mhead_def)