diff -r a910a65478be -r d199410f1db1 HOL.thy
--- a/HOL.thy	Tue Sep 28 14:27:31 1993 +0100
+++ b/HOL.thy	Mon Oct 04 15:43:54 1993 +0100
@@ -28,41 +28,42 @@
 
   (* Constants *)
 
-  Trueprop      :: "bool => prop"                       ("(_)" [0] 5)
-  not           :: "bool => bool"                       ("~ _" [40] 40)
+  Trueprop      :: "bool => prop"                     ("(_)" 5)
+  not           :: "bool => bool"                     ("~ _" [40] 40)
   True, False   :: "bool"
   if            :: "[bool, 'a, 'a] => 'a"
   Inv           :: "('a => 'b) => ('b => 'a)"
 
   (* Binders *)
 
-  Eps           :: "('a => bool) => 'a"                 (binder "@" 10)
-  All           :: "('a => bool) => bool"               (binder "! " 10)
-  Ex            :: "('a => bool) => bool"               (binder "? " 10)
-  Ex1           :: "('a => bool) => bool"               (binder "?! " 10)
+  Eps           :: "('a => bool) => 'a"               (binder "@" 10)
+  All           :: "('a => bool) => bool"             (binder "! " 10)
+  Ex            :: "('a => bool) => bool"             (binder "? " 10)
+  Ex1           :: "('a => bool) => bool"             (binder "?! " 10)
 
-  Let		:: "['a, 'a=>'b] => 'b"
-  "@let"	:: "[idt,'a,'b] => 'b"		("(let _ = (2_)/ in (2_))" 10)
+  Let           :: "['a, 'a => 'b] => 'b"
+  "@Let"        :: "[idt, 'a, 'b] => 'b"              ("(let _ = (2_)/ in (2_))" 10)
 
   (* Alternative Quantifiers *)
 
-  "*All"        :: "[idts, bool] => bool"             ("(3ALL _./ _)" [0,0] 10)
-  "*Ex"         :: "[idts, bool] => bool"             ("(3EX _./ _)" [0,0] 10)
-  "*Ex1"        :: "[idts, bool] => bool"             ("(3EX! _./ _)" [0,0] 10)
+  "*The"        :: "[idts, bool] => 'a"               ("(3THE _./ _)" 10)
+  "*All"        :: "[idts, bool] => bool"             ("(3ALL _./ _)" 10)
+  "*Ex"         :: "[idts, bool] => bool"             ("(3EX _./ _)" 10)
+  "*Ex1"        :: "[idts, bool] => bool"             ("(3EX! _./ _)" 10)
 
   (* Infixes *)
 
-  o             :: "['b => 'c, 'a => 'b, 'a] => 'c"     (infixr 50)
-  "="           :: "['a, 'a] => bool"                   (infixl 50)
-  "&"           :: "[bool, bool] => bool"               (infixr 35)
-  "|"           :: "[bool, bool] => bool"               (infixr 30)
-  "-->"         :: "[bool, bool] => bool"               (infixr 25)
+  o             :: "['b => 'c, 'a => 'b, 'a] => 'c"   (infixr 50)
+  "="           :: "['a, 'a] => bool"                 (infixl 50)
+  "&"           :: "[bool, bool] => bool"             (infixr 35)
+  "|"           :: "[bool, bool] => bool"             (infixr 30)
+  "-->"         :: "[bool, bool] => bool"             (infixr 25)
 
   (* Overloaded Constants *)
 
-  "+"           :: "['a::plus, 'a] => 'a"               (infixl 65)
-  "-"           :: "['a::minus, 'a] => 'a"              (infixl 65)
-  "*"           :: "['a::times, 'a] => 'a"              (infixl 70)
+  "+"           :: "['a::plus, 'a] => 'a"             (infixl 65)
+  "-"           :: "['a::minus, 'a] => 'a"            (infixl 65)
+  "*"           :: "['a::times, 'a] => 'a"            (infixl 70)
 
   (* Rewriting Gadget *)
 
@@ -70,11 +71,12 @@
 
 
 translations
+  "THE xs. P"   => "@ xs. P"
   "ALL xs. P"   => "! xs. P"
   "EX xs. P"    => "? xs. P"
   "EX! xs. P"   => "?! xs. P"
 
-  "let x = s in t" == "Let(s,%x.t)"
+  "let x = s in t" == "Let(s, %x. t)"
 
 rules
 
@@ -100,7 +102,7 @@
   and_def       "op & = (%P Q. !R. (P-->Q-->R) --> R)"
   or_def        "op | = (%P Q. !R. (P-->R) --> (Q-->R) --> R)"
   Ex1_def       "Ex1  = (%P. ? x. P(x) & (! y. P(y) --> y=x))"
-  Let_def	"Let(s,f) = f(s)"
+  Let_def       "Let(s, f) = f(s)"
 
   (* Axioms *)
 
@@ -127,16 +129,16 @@
 
 val HOL_quantifiers = ref true;
 
-fun mk_alt_ast_tr' (name, alt_name) =
+fun alt_ast_tr' (name, alt_name) =
   let
     fun ast_tr' (*name*) args =
       if ! HOL_quantifiers then raise Match
-      else Ast.mk_appl (Ast.Constant alt_name) args;
+      else Syntax.mk_appl (Syntax.Constant alt_name) args;
   in
     (name, ast_tr')
   end;
 
 
 val print_ast_translation =
-  map mk_alt_ast_tr' [("! ", "*All"), ("? ", "*Ex"), ("?! ", "*Ex1")];
+  map alt_ast_tr' [("@", "*The"), ("! ", "*All"), ("? ", "*Ex"), ("?! ", "*Ex1")];