diff -r a32d357dfd70 -r 361e62500ab7 src/HOL/Code_Generator.thy
--- a/src/HOL/Code_Generator.thy	Fri Oct 20 10:44:35 2006 +0200
+++ b/src/HOL/Code_Generator.thy	Fri Oct 20 10:44:36 2006 +0200
@@ -115,7 +115,9 @@
   fixes eq :: "'a \<Rightarrow> 'a \<Rightarrow> bool"
 
 defs
-  eq_def: "eq x y \<equiv> (x = y)"
+  eq_def [normal post]: "eq \<equiv> (op =)"
+
+lemmas [symmetric, code inline] = eq_def
 
 
 subsubsection {* bool type *}
@@ -134,9 +136,6 @@
 lemma [code func]:
   "eq p False = (\<not> p)" unfolding eq_def by auto
 
-code_constname
-  "eq \<Colon> bool \<Rightarrow> bool \<Rightarrow> bool" "HOL.eq_bool"
-
 
 subsubsection {* preprocessors *}
 
@@ -155,8 +154,6 @@
 in CodegenData.add_constrains constrain_op_eq end
 *}
 
-declare eq_def [symmetric, code inline]
-
 
 subsubsection {* Haskell *}
 
@@ -190,6 +187,22 @@
 end;
 *}
 
-hide (open) const eq
+text {* lazy @{const If} *}
+
+definition
+  if_delayed :: "bool \<Rightarrow> (bool \<Rightarrow> 'a) \<Rightarrow> (bool \<Rightarrow> 'a) \<Rightarrow> 'a"
+  "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"
+  unfolding if_delayed_def by simp_all
+
+lemma [normal pre, symmetric, normal post]:
+  "(if b then x else y) = if_delayed b (\<lambda>_. x) (\<lambda>_. y)"
+  unfolding if_delayed_def ..
+
+
+hide (open) const eq if_delayed
 
 end
\ No newline at end of file