diff -r 0a2a1b6507c1 -r 493b818e8e10 src/HOL/HOL.thy
--- a/src/HOL/HOL.thy	Wed Apr 18 21:12:50 2018 +0100
+++ b/src/HOL/HOL.thy	Wed May 02 13:49:38 2018 +0200
@@ -1398,6 +1398,9 @@
 lemma if_distrib: "f (if c then x else y) = (if c then f x else f y)"
   by simp
 
+lemma if_distribR: "(if b then f else g) x = (if b then f x else g x)"
+  by simp
+
 lemma all_if_distrib: "(\<forall>x. if x = a then P x else Q x) \<longleftrightarrow> P a \<and> (\<forall>x. x\<noteq>a \<longrightarrow> Q x)"
   by auto