diff -r a88e16b69d0f -r 9d35c6145dd2 Attic/Unused.thy
--- a/Attic/Unused.thy	Thu Jan 28 10:52:10 2010 +0100
+++ b/Attic/Unused.thy	Thu Jan 28 12:24:49 2010 +0100
@@ -6,9 +6,9 @@
   by(auto simp add: QUOT_TRUE_def)
 
 syntax
-  "Bexeq" :: "id \<Rightarrow> ('a \<Rightarrow> 'a \<Rightarrow> bool) \<Rightarrow> ('a \<Rightarrow> bool) \<Rightarrow> bool" ("(3\<exists>!!_\<in>_./ _)" [0, 0, 10] 10)
+  "Bex1_rel" :: "id \<Rightarrow> ('a \<Rightarrow> 'a \<Rightarrow> bool) \<Rightarrow> ('a \<Rightarrow> bool) \<Rightarrow> bool" ("(3\<exists>!!_\<in>_./ _)" [0, 0, 10] 10)
 translations
-  "\<exists>!!x\<in>A. P"  == "Bexeq A (%x. P)"
+  "\<exists>!!x\<in>A. P"  == "Bex1_rel A (%x. P)"
 
 
 (* Atomize infrastructure *)