diff -r c16135580a45 -r af57c9723fae Quot/Nominal/Test.thy
--- a/Quot/Nominal/Test.thy	Wed Jan 27 17:18:30 2010 +0100
+++ b/Quot/Nominal/Test.thy	Wed Jan 27 17:39:13 2010 +0100
@@ -265,7 +265,7 @@
 binder
   f::"pat \<Rightarrow> name set"
 where 
-  "f PN = {}"
+  "f PN = ({} :: name set)"
 | "f (PS x) = {x}"
 | "f (PD (x,y)) = {x,y}"
 
@@ -281,9 +281,9 @@
 binder
   f2::"pat2 \<Rightarrow> name set"
 where 
-  "f2 PN2 = {}"
+  "f2 PN2 = ({} :: name set)"
 | "f2 (PS2 x) = {x}"
-| "f2 (PD2 (p1, p2)) = (f2 p1) \<union> (f2 p2)"
+| "f2 (PD2 (p1, p2)) = (f2 p1) \<union> (f2 p2 :: name set)"
 
 text {* example type schemes *}
 datatype ty =