--- a/univ.thy	Thu Mar 17 14:08:08 1994 +0100
+++ b/univ.thy	Thu Mar 17 17:02:49 1994 +0100
@@ -12,8 +12,13 @@
 *)
 
 Univ = Arith +
-types   node 1
-arities node :: (term)term
+
+types
+  'a node
+
+arities
+  node :: (term)term
+
 consts
   Least     :: "(nat=>bool) => nat"    (binder "LEAST " 10)