--- a/Nominal/ExPS3.thy	Fri Mar 26 10:55:13 2010 +0100
+++ b/Nominal/ExPS3.thy	Fri Mar 26 16:20:39 2010 +0100
@@ -11,17 +11,17 @@
   VarP "name"
 | AppP "exp" "exp"
 | LamP x::"name" e::"exp" bind x in e
-| LetP x::"name" p::"pat3" e1::"exp" e2::"exp" bind x in e2, bind "bp'' p" in e1
+| LetP x::"name" p::"pat3" e1::"exp" e2::"exp" bind x in e2, bind "bp p" in e1
 and pat3 =
   PVar "name"
 | PUnit
 | PPair "pat3" "pat3"
 binder
-  bp'' :: "pat3 \<Rightarrow> atom set"
+  bp :: "pat3 \<Rightarrow> atom set"
 where
-  "bp'' (PVar x) = {atom x}"
-| "bp'' (PUnit) = {}"
-| "bp'' (PPair p1 p2) = bp'' p1 \<union> bp'' p2"
+  "bp (PVar x) = {atom x}"
+| "bp (PUnit) = {}"
+| "bp (PPair p1 p2) = bp p1 \<union> bp p2"
 
 thm exp_pat3.fv
 thm exp_pat3.eq_iff
@@ -30,7 +30,7 @@
 thm exp_pat3.induct
 thm exp_pat3.distinct
 thm exp_pat3.fv
-thm exp_pat3.supp (* The bindings are too complicated *)
+thm exp_pat3.supp
 
 end