diff -r d1d09177ec89 -r 3ce1089cdbf3 Nominal/Ex/Shallow.thy
--- a/Nominal/Ex/Shallow.thy	Fri Dec 31 13:31:39 2010 +0000
+++ b/Nominal/Ex/Shallow.thy	Fri Dec 31 15:37:04 2010 +0000
@@ -32,9 +32,9 @@
 nominal_datatype trm3 =
   Var3 "name"
 | App3 "trm3" "trm3"
-| Lam3 xs::"name fset" t::"trm3" bind (res) xs in t
+| Lam3 xs::"name fset" t::"trm3" bind (set+) xs in t
 
-thm trm3.strong_exhaust
+thm trm3.eq_iff
 
 end