1.1 --- a/src/HOL/HOL.thy	Sat Jul 02 22:14:47 2011 +0200
     1.2 +++ b/src/HOL/HOL.thy	Sat Jul 02 22:55:58 2011 +0200
     1.3 @@ -1892,14 +1892,8 @@
     1.4    shows "CASE x \<equiv> f x"
     1.5    using assms by simp_all
     1.6  
     1.7 -lemma If_case_cert:
     1.8 -  assumes "CASE \<equiv> (\<lambda>b. If b f g)"
     1.9 -  shows "(CASE True \<equiv> f) &&& (CASE False \<equiv> g)"
    1.10 -  using assms by simp_all
    1.11 -
    1.12  setup {*
    1.13    Code.add_case @{thm Let_case_cert}
    1.14 -  #> Code.add_case @{thm If_case_cert}
    1.15    #> Code.add_undefined @{const_name undefined}
    1.16  *}
    1.17  

     2.1 --- a/src/HOL/Product_Type.thy	Sat Jul 02 22:14:47 2011 +0200
     2.2 +++ b/src/HOL/Product_Type.thy	Sat Jul 02 22:55:58 2011 +0200
     2.3 @@ -28,6 +28,15 @@
     2.4      and [code nbe]: "HOL.equal P P \<longleftrightarrow> True"
     2.5    by (simp_all add: equal)
     2.6  
     2.7 +lemma If_case_cert:
     2.8 +  assumes "CASE \<equiv> (\<lambda>b. If b f g)"
     2.9 +  shows "(CASE True \<equiv> f) &&& (CASE False \<equiv> g)"
    2.10 +  using assms by simp_all
    2.11 +
    2.12 +setup {*
    2.13 +  Code.add_case @{thm If_case_cert}
    2.14 +*}
    2.15 +
    2.16  code_const "HOL.equal \<Colon> bool \<Rightarrow> bool \<Rightarrow> bool"
    2.17    (Haskell infix 4 "==")
    2.18