diff -r 0fba0357c04c -r c77e5401f2ff src/HOL/Induct/Sexp.thy
--- a/src/HOL/Induct/Sexp.thy	Wed Aug 08 14:50:28 2001 +0200
+++ b/src/HOL/Induct/Sexp.thy	Wed Aug 08 14:51:10 2001 +0200
@@ -28,9 +28,9 @@
 defs
 
   sexp_case_def 
-   "sexp_case c d e M == @ z. (? x.   M=Leaf(x) & z=c(x))  
-                            | (? k.   M=Numb(k) & z=d(k))  
-                            | (? N1 N2. M = Scons N1 N2  & z=e N1 N2)"
+   "sexp_case c d e M == THE z. (EX x.   M=Leaf(x) & z=c(x))  
+                            | (EX k.   M=Numb(k) & z=d(k))  
+                            | (EX N1 N2. M = Scons N1 N2  & z=e N1 N2)"
 
   pred_sexp_def
      "pred_sexp == UN M: sexp. UN N: sexp. {(M, Scons M N), (N, Scons M N)}"