--- a/LamEx.thy	Mon Nov 30 10:16:10 2009 +0100
+++ b/LamEx.thy	Mon Nov 30 11:53:20 2009 +0100
@@ -171,8 +171,7 @@
 
 ML {* val qty = @{typ "lam"} *}
 ML {* val defs = @{thms Var_def App_def Lam_def perm_lam_def fv_def} *}
-ML {* val rsp_thms = @{thms perm_rsp fresh_rsp rVar_rsp rApp_rsp rLam_rsp rfv_rsp} @
-  @{thms ho_all_prs ho_ex_prs} *}
+ML {* val rsp_thms = @{thms perm_rsp fresh_rsp rVar_rsp rApp_rsp rLam_rsp rfv_rsp} *}
 
 ML {* val (rty, rel, rel_refl, rel_eqv) = lookup_quot_data @{context} qty *}
 ML {* val consts = lookup_quot_consts defs *}