src/HOL/UNITY/Lift_prog.thy

--- a/src/HOL/UNITY/Lift_prog.thy	Tue Feb 23 15:37:18 2016 +0100
+++ b/src/HOL/UNITY/Lift_prog.thy	Tue Feb 23 16:25:08 2016 +0100
@@ -129,7 +129,7 @@
       ==> \<exists>g'. insert_map i s' f = insert_map j t g'"
 apply (subst insert_map_upd_same [symmetric])
 apply (erule ssubst)
-apply (simp only: insert_map_upd if_False split: split_if, blast)
+apply (simp only: insert_map_upd if_False split: if_split, blast)
 done
 
 lemma lift_map_eq_diff: