src/HOL/Bali/Evaln.thy

 	        G\<turnstile>set_lvars empty s1 \<midarrow>init c\<midarrow>n\<rightarrow> s2 \<and> 
                 s3 = restore_lvars s1 s2)\<rbrakk>
           \<Longrightarrow>
 		 G\<turnstile>Norm s0 \<midarrow>Init C\<midarrow>n\<rightarrow> s3"
 monos
-  if_def2
+  if_bool_eq_conj
 
 
 declare split_if     [split del] split_if_asm     [split del]
         option.split [split del] option.split_asm [split del]
         not_None_eq [simp del]