src/HOL/Code_Generator.thy

 *}
 
 text {* lazy @{const If} *}
 
 definition
-  if_delayed :: "bool \<Rightarrow> (bool \<Rightarrow> 'a) \<Rightarrow> (bool \<Rightarrow> 'a) \<Rightarrow> 'a"
+  if_delayed :: "bool \<Rightarrow> (bool \<Rightarrow> 'a) \<Rightarrow> (bool \<Rightarrow> 'a) \<Rightarrow> 'a" where
   "if_delayed b f g = (if b then f True else g False)"
 
 lemma [code func]:
   shows "if_delayed True f g = f True"
     and "if_delayed False f g = g False"