--- a/Nominal/Ex/ExPS8.thy	Wed Aug 25 23:16:42 2010 +0800
+++ b/Nominal/Ex/ExPS8.thy	Thu Aug 26 02:08:00 2010 +0800
@@ -6,17 +6,13 @@
 
 atom_decl name
 
-ML {* val _ = cheat_fv_rsp := true *}
-ML {* val _ = cheat_equivp := true *}
-ML {* val _ = cheat_alpha_bn_rsp := true *}
-
 nominal_datatype exp =
   EVar name
 | EUnit
 | EPair exp exp
-| ELetRec l::lrbs e::exp bind_set "b_lrbs l" in l e
+| ELetRec l::lrbs e::exp bind (set) "b_lrbs l" in l e
 and fnclause =
-  K x::name p::pat f::exp bind_set "b_pat p" in f
+  K x::name p::pat f::exp bind (set) "b_pat p" in f
 and fnclauses =
   S fnclause
 | ORs fnclause fnclauses
@@ -46,8 +42,6 @@
 | "b_lrb (Clause fcs) = (b_fnclauses fcs)"
 | "b_fnclause (K x pat exp) = {atom x}"
 
-thm exp_fnclause_fnclauses_lrb_lrbs_pat.fv
-thm exp_fnclause_fnclauses_lrb_lrbs_pat.eq_iff
 
 end