src/HOL/HOL.thy

--- a/src/HOL/HOL.thy	Mon Oct 20 11:22:29 1997 +0200
+++ b/src/HOL/HOL.thy	Mon Oct 20 11:25:39 1997 +0200
@@ -11,6 +11,8 @@
 
 (** Core syntax **)
 
+global
+
 classes
   term < logic
 
@@ -33,6 +35,7 @@
   Not           :: bool => bool                     ("~ _" [40] 40)
   True, False   :: bool
   If            :: [bool, 'a, 'a] => 'a   ("(if (_)/ then (_)/ else (_))" 10)
+  arbitrary     :: 'a
 
   (* Binders *)
 
@@ -141,6 +144,8 @@
 
 (** Rules and definitions **)
 
+local
+
 rules
 
   eq_reflection "(x=y) ==> (x==y)"
@@ -179,9 +184,6 @@
   o_def         "(f::'b=>'c) o g == (%(x::'a). f(g(x)))"
   if_def        "If P x y == @z::'a. (P=True --> z=x) & (P=False --> z=y)"
 
-consts
-  arbitrary :: 'a
-
 
 end