diff -r d9527f97246e -r 89669c58e506 Univ.thy
--- a/Univ.thy	Thu Aug 25 10:47:33 1994 +0200
+++ b/Univ.thy	Thu Aug 25 11:01:45 1994 +0200
@@ -15,6 +15,7 @@
 
 types
   'a node
+  'a item = "'a node set"
 
 arities
   node :: (term)term
@@ -31,25 +32,25 @@
   Push_Node :: "[nat, 'a node] => 'a node"
   ndepth    :: "'a node => nat"
 
-  Atom      :: "('a+nat) => 'a node set"
-  Leaf      :: "'a => 'a node set"
-  Numb      :: "nat => 'a node set"
-  "$"       :: "['a node set, 'a node set]=> 'a node set" 	(infixr 60)
-  In0,In1   :: "'a node set => 'a node set"
+  Atom      :: "('a+nat) => 'a item"
+  Leaf      :: "'a => 'a item"
+  Numb      :: "nat => 'a item"
+  "$"       :: "['a item, 'a item]=> 'a item" 	(infixr 60)
+  In0,In1   :: "'a item => 'a item"
 
-  ntrunc    :: "[nat, 'a node set] => 'a node set"
+  ntrunc    :: "[nat, 'a item] => 'a item"
 
-  "<*>"  :: "['a node set set, 'a node set set]=> 'a node set set" (infixr 80)
-  "<+>"  :: "['a node set set, 'a node set set]=> 'a node set set" (infixr 70)
+  "<*>"  :: "['a item set, 'a item set]=> 'a item set" (infixr 80)
+  "<+>"  :: "['a item set, 'a item set]=> 'a item set" (infixr 70)
 
-  Split	 :: "[['a node set, 'a node set]=>'b, 'a node set] => 'b"
-  Case   :: "[['a node set]=>'b, ['a node set]=>'b, 'a node set] => 'b"
+  Split	 :: "[['a item, 'a item]=>'b, 'a item] => 'b"
+  Case   :: "[['a item]=>'b, ['a item]=>'b, 'a item] => 'b"
 
   diag   :: "'a set => ('a * 'a)set"
-  "<**>" :: "[('a node set * 'a node set)set, ('a node set * 'a node set)set] \
-\           => ('a node set * 'a node set)set" (infixr 80)
-  "<++>" :: "[('a node set * 'a node set)set, ('a node set * 'a node set)set] \
-\           => ('a node set * 'a node set)set" (infixr 70)
+  "<**>" :: "[('a item * 'a item)set, ('a item * 'a item)set] \
+\           => ('a item * 'a item)set" (infixr 80)
+  "<++>" :: "[('a item * 'a item)set, ('a item * 'a item)set] \
+\           => ('a item * 'a item)set" (infixr 70)
 
 rules