emilimated global names;

--- a/src/HOL/Univ.thy	Tue Apr 18 14:54:08 2000 +0200
+++ b/src/HOL/Univ.thy	Tue Apr 18 14:57:18 2000 +0200
@@ -16,8 +16,6 @@
 
 (** lists, trees will be sets of nodes **)
 
-global
-
 typedef (Node)
   ('a, 'b) node = "{p. EX f x k. p = (f::nat=>'b+nat, x::'a+nat) & f k = Inr 0}"
 
@@ -55,8 +53,6 @@
                 => (('a, 'b) dtree * ('a, 'b) dtree)set"
 
 
-local
-
 defs
 
   Push_Node_def  "Push_Node == (%n x. Abs_Node (apfst (Push n) (Rep_Node x)))"