src/HOL/Bali/Conform.thy

       \<forall>vs Ts. distinct vns \<longrightarrow> length Ts = length vns 
       \<longrightarrow> list_all2 (conf G s) vs Ts \<longrightarrow> G,s\<turnstile>l(vns[\<mapsto>]vs)[\<Colon>\<preceq>]L(vns[\<mapsto>]Ts)"
 apply (unfold lconf_def)
 apply (induct_tac "vns")
 apply  clarsimp
-apply clarsimp
+apply clarify
 apply (frule list_all2_lengthD)
-apply clarsimp
+apply (clarsimp)
 done
 
 
 lemma lconf_deallocL: "\<lbrakk>G,s\<turnstile>l[\<Colon>\<preceq>]L(vn\<mapsto>T); L vn = None\<rbrakk> \<Longrightarrow> G,s\<turnstile>l[\<Colon>\<preceq>]L"
 apply (simp only: lconf_def)

       \<forall>vs Ts. distinct vns \<longrightarrow> length Ts = length vns 
       \<longrightarrow> list_all2 (conf G s) vs Ts \<longrightarrow> G,s\<turnstile>l(vns[\<mapsto>]vs)[\<sim>\<Colon>\<preceq>]L(vns[\<mapsto>]Ts)"
 apply (unfold wlconf_def)
 apply (induct_tac "vns")
 apply  clarsimp
-apply clarsimp
+apply clarify
 apply (frule list_all2_lengthD)
 apply clarsimp
 done