Fix the problem with later examples. Maybe need to go back to textual specifications.
authorCezary Kaliszyk <kaliszyk@in.tum.de>
Wed, 27 Jan 2010 17:39:13 +0100
changeset 971 af57c9723fae
parent 970 c16135580a45
child 972 9913c5695fc7
Fix the problem with later examples. Maybe need to go back to textual specifications.
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 =