# HG changeset patch
# User wenzelm
# Date 956062638 -7200
# Node ID bb2250ac955767e26412c44e318f518c8e1700b0
# Parent  b456aba346a6fda41009d63eeb6c3ed561ee3f98
emilimated global names;

diff -r b456aba346a6 -r bb2250ac9557 src/HOL/Univ.thy
--- 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)))"