diff -r 963aff0818c2 -r 1ea751ae62b2 src/HOL/Lambda/Lambda.thy
--- a/src/HOL/Lambda/Lambda.thy	Wed Jul 15 11:15:57 1998 +0200
+++ b/src/HOL/Lambda/Lambda.thy	Wed Jul 15 12:02:19 1998 +0200
@@ -9,7 +9,7 @@
 
 Lambda = Arith + Inductive +
 
-datatype dB = Var nat | "@" dB dB (infixl 200) | Abs dB
+datatype dB = Var nat | "$" dB dB (infixl 200) | Abs dB
 
 consts
   subst  :: [dB,dB,nat]=>dB ("_[_'/_]" [300,0,0] 300)
@@ -20,24 +20,24 @@
 
 primrec lift dB
   "lift (Var i) k = (if i < k then Var i else Var(Suc i))"
-  "lift (s @ t) k = (lift s k) @ (lift t k)"
+  "lift (s $ t) k = (lift s k) $ (lift t k)"
   "lift (Abs s) k = Abs(lift s (Suc k))"
 
 primrec subst dB
   subst_Var "(Var i)[s/k] = (if k < i then Var(i-1)
                             else if i = k then s else Var i)"
-  subst_App "(t @ u)[s/k] = t[s/k] @ u[s/k]"
+  subst_App "(t $ u)[s/k] = t[s/k] $ u[s/k]"
   subst_Abs "(Abs t)[s/k] = Abs (t[lift s 0 / Suc k])"
 
 primrec liftn dB
   "liftn n (Var i) k = (if i < k then Var i else Var(i+n))"
-  "liftn n (s @ t) k = (liftn n s k) @ (liftn n t k)"
+  "liftn n (s $ t) k = (liftn n s k) $ (liftn n t k)"
   "liftn n (Abs s) k = Abs(liftn n s (Suc k))"
 
 primrec substn dB
   "substn (Var i) s k = (if k < i then Var(i-1)
                          else if i = k then liftn k s 0 else Var i)"
-  "substn (t @ u) s k = (substn t s k) @ (substn u s k)"
+  "substn (t $ u) s k = (substn t s k) $ (substn u s k)"
   "substn (Abs t) s k = Abs (substn t s (Suc k))"
 
 consts  beta :: "(dB * dB) set"
@@ -50,8 +50,8 @@
 
 inductive beta
 intrs
-   beta  "(Abs s) @ t -> s[t/0]"
-   appL  "s -> t ==> s@u -> t@u"
-   appR  "s -> t ==> u@s -> u@t"
+   beta  "(Abs s) $ t -> s[t/0]"
+   appL  "s -> t ==> s$u -> t$u"
+   appR  "s -> t ==> u$s -> u$t"
    abs   "s -> t ==> Abs s -> Abs t"
 end