src/HOL/Univ.thy

--- a/src/HOL/Univ.thy	Fri Dec 01 13:54:27 1995 +0100
+++ b/src/HOL/Univ.thy	Fri Dec 01 14:17:50 1995 +0100
@@ -19,7 +19,7 @@
   'a node = "{p. EX f x k. p = (f::nat=>nat, x::'a+nat) & f(k)=0}"
 
 types
-  'a item = "'a node set"
+  'a item = 'a node set
 
 consts
   Least     :: (nat=>bool) => nat    (binder "LEAST " 10)