--- a/src/HOL/Extraction.thy Thu Dec 09 18:30:59 2004 +0100
+++ b/src/HOL/Extraction.thy Fri Dec 10 16:47:15 2004 +0100
@@ -213,8 +213,8 @@
"P y x \<Longrightarrow> P (snd (x, y)) (fst (x, y))" by simp
theorem exE_realizer: "P (snd p) (fst p) \<Longrightarrow>
- (\<And>x y. P y x \<Longrightarrow> Q (f x y)) \<Longrightarrow> Q (case p of (x, y) \<Rightarrow> f x y)"
- by (cases p) simp
+ (\<And>x y. P y x \<Longrightarrow> Q (f x y)) \<Longrightarrow> Q (let (x, y) = p in f x y)"
+ by (cases p) (simp add: Let_def)
theorem exE_realizer': "P (snd p) (fst p) \<Longrightarrow>
(\<And>x y. P y x \<Longrightarrow> Q) \<Longrightarrow> Q" by (cases p) simp
@@ -252,7 +252,7 @@
exI: "\<lambda>x. x" "\<Lambda> P x (h: _). h"
- exE (P, Q): "\<lambda>p pq. case p of (x, y) \<Rightarrow> pq x y"
+ exE (P, Q): "\<lambda>p pq. let (x, y) = p in pq x y"
"\<Lambda> P Q p (h: _) pq. exE_realizer \<cdot> P \<cdot> p \<cdot> Q \<cdot> pq \<bullet> h"
exE (P): "Null"