# HG changeset patch
# User berghofe
# Date 1102693635 -3600
# Node ID 2e6a9146caca9efeb455cc0b7a5a88b1d473bb4b
# Parent  290bc97038c704c4cf60b20f5c8e4b51065d6459
Realizer for exE now uses let instead of case.

diff -r 290bc97038c7 -r 2e6a9146caca src/HOL/Extraction.thy
--- 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"