src/HOL/Univ.thy

--- a/src/HOL/Univ.thy	Mon Oct 20 11:22:29 1997 +0200
+++ b/src/HOL/Univ.thy	Mon Oct 20 11:25:39 1997 +0200
@@ -13,6 +13,8 @@
 
 (** lists, trees will be sets of nodes **)
 
+global
+
 typedef (Node)
   'a node = "{p. EX f x k. p = (f::nat=>nat, x::'a+nat) & f(k)=0}"
 
@@ -46,6 +48,9 @@
   "<++>" :: "[('a item * 'a item)set, ('a item * 'a item)set] 
            => ('a item * 'a item)set" (infixr 70)
 
+
+local
+
 defs
 
   Push_Node_def  "Push_Node == (%n x. Abs_Node (apfst (Push n) (Rep_Node x)))"