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