--- a/src/HOL/Univ.thy Mon Feb 05 14:44:09 1996 +0100
+++ b/src/HOL/Univ.thy Mon Feb 05 21:27:16 1996 +0100
@@ -15,7 +15,7 @@
(** lists, trees will be sets of nodes **)
-subtype (Node)
+typedef (Node)
'a node = "{p. EX f x k. p = (f::nat=>nat, x::'a+nat) & f(k)=0}"
types