# HG changeset patch
# User haftmann
# Date 1330804831 -3600
# Node ID d50855d9ea74f5f318088969e8caf496dc7902af
# Parent  4ec6bd791ee9776c615b4fe94b0fab8882daf4e4
spurious set/pred correction

diff -r 4ec6bd791ee9 -r d50855d9ea74 src/HOL/Import/HOLLightCompat.thy
--- a/src/HOL/Import/HOLLightCompat.thy	Sat Mar 03 21:00:24 2012 +0100
+++ b/src/HOL/Import/HOLLightCompat.thy	Sat Mar 03 21:00:31 2012 +0100
@@ -192,8 +192,8 @@
   by auto
 
 lemma DEF_INSERT:
-  "insert = (%u ua y. y \<in> ua | y = u)"
-  unfolding mem_def fun_eq_iff insert_code by blast
+  "insert = (\<lambda>u ua. {y. y \<in> ua | y = u})"
+  by auto
 
 lemma DEF_IMAGE:
   "op ` = (\<lambda>u ua. {ub. \<exists>y. (\<exists>x. x \<in> ua \<and> y = u x) \<and> ub = y})"
@@ -331,8 +331,8 @@
 
 lemmas [hol4rew] = id_apply
 
-lemma DEF_CHOICE: "Eps = (%u. SOME x. x \<in> u)"
-  by (simp add: mem_def)
+lemma DEF_CHOICE: "Eps = (%u. SOME x. u x)"
+  by simp
 
 definition dotdot :: "nat => nat => nat set"
   where "dotdot u ua = {ub. EX x. (u <= x & x <= ua) & ub = x}"
@@ -347,3 +347,4 @@
   by (simp add: INFINITE_def_raw)
 
 end
+