diff -r 428d9cb9a243 -r 49ab06c0ca64 Nominal/Ex/SingleLet.thy
--- a/Nominal/Ex/SingleLet.thy	Tue Aug 17 07:11:45 2010 +0800
+++ b/Nominal/Ex/SingleLet.thy	Tue Aug 17 17:52:25 2010 +0800
@@ -25,6 +25,8 @@
 
 thm distinct
 thm trm_raw_assg_raw.inducts
+thm trm_raw.exhaust
+thm assg_raw.exhaust
 thm fv_defs
 thm perm_simps
 thm perm_laws
@@ -37,8 +39,6 @@
 thm size_eqvt
 
 
-(* eqvt lemmas for fv / fv_bn / bn *)
-
 ML {*
   val thms_d = map (lift_thm [@{typ trm}, @{typ assg}] @{context}) @{thms distinct}
 *}
@@ -47,6 +47,14 @@
   val thms_i = map (lift_thm [@{typ trm}, @{typ assg}] @{context}) @{thms trm_raw_assg_raw.inducts}
 *}
 
+ML {* 
+  val thms_i = map (lift_thm [@{typ trm}, @{typ assg}] @{context}) @{thms trm_raw.exhaust}
+*}
+
+ML {* 
+  val thms_i = map (lift_thm [@{typ trm}, @{typ assg}] @{context}) @{thms assg_raw.exhaust}
+*}
+
 ML {*
   val thms_f = map (lift_thm [@{typ trm}, @{typ assg}] @{context}) @{thms fv_defs}
 *}