--- a/Nominal/Ex/ExPS7.thy	Wed Aug 25 23:16:42 2010 +0800
+++ b/Nominal/Ex/ExPS7.thy	Thu Aug 26 02:08:00 2010 +0800
@@ -11,7 +11,7 @@
   Var name
 | Unit
 | Pair exp exp
-| LetRec l::"lrbs" e::"exp"  bind_set "bs l" in l e
+| LetRec l::"lrbs" e::"exp"  bind (set) "bs l" in l e
 and lrb =
   Assign name exp
 and lrbs =
@@ -25,8 +25,6 @@
 | "bs (Single a) = b a"
 | "bs (More a as) = (b a) \<union> (bs as)"
 
-thm exp_lrb_lrbs.eq_iff
-thm exp_lrb_lrbs.supp
 
 
 end