diff -r 1dad51c852ad -r 3f2144aebd76 src/HOL/Hilbert_Choice.thy
--- a/src/HOL/Hilbert_Choice.thy	Sat Jun 05 13:06:49 2004 +0200
+++ b/src/HOL/Hilbert_Choice.thy	Sat Jun 05 13:07:04 2004 +0200
@@ -15,8 +15,8 @@
 consts
   Eps           :: "('a => bool) => 'a"
 
-syntax (input)
-  "_Eps"        :: "[pttrn, bool] => 'a"    ("(3\<epsilon>_./ _)" [0, 10] 10)
+syntax (epsilon)
+  "_Eps"        :: "[pttrn, bool] => 'a"    ("(3\<some>_./ _)" [0, 10] 10)
 syntax (HOL)
   "_Eps"        :: "[pttrn, bool] => 'a"    ("(3@ _./ _)" [0, 10] 10)
 syntax