diff -r ea46a354f382 -r 6a133abb7633 Nominal/Term1.thy
--- a/Nominal/Term1.thy	Fri Feb 26 18:21:39 2010 +0100
+++ b/Nominal/Term1.thy	Fri Feb 26 18:38:25 2010 +0100
@@ -39,7 +39,7 @@
   alpha_rtrm1 ("_ \<approx>1 _" [100, 100] 100) and
   alpha_bp ("_ \<approx>1b _" [100, 100] 100)
 thm alpha_rtrm1_alpha_bp.intros
-thm fv_rtrm1_fv_bp.simps
+thm fv_rtrm1_fv_bp.simps[no_vars]
 
 local_setup {* (fn ctxt => snd (Local_Theory.note ((@{binding alpha1_inj}, []), (build_alpha_inj @{thms alpha_rtrm1_alpha_bp.intros} @{thms rtrm1.distinct rtrm1.inject bp.distinct bp.inject} @{thms alpha_rtrm1.cases alpha_bp.cases} ctxt)) ctxt)) *}
 thm alpha1_inj