--- 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)