diff -r aec9576b3950 -r 06ace3a1eedd Quot/Nominal/Fv.thy
--- a/Quot/Nominal/Fv.thy	Mon Feb 22 17:19:28 2010 +0100
+++ b/Quot/Nominal/Fv.thy	Mon Feb 22 18:09:44 2010 +0100
@@ -220,11 +220,11 @@
 ML {*
 fun alpha_inj_tac dist_inj intrs elims =
   SOLVED' (asm_full_simp_tac (HOL_ss addsimps intrs)) ORELSE'
-  rtac @{thm iffI} THEN' RANGE [
+  (rtac @{thm iffI} THEN' RANGE [
      (eresolve_tac elims THEN_ALL_NEW
        asm_full_simp_tac (HOL_ss addsimps dist_inj)
      ),
-     (asm_full_simp_tac (HOL_ss addsimps intrs))]
+     asm_full_simp_tac (HOL_ss addsimps intrs)])
 *}
 
 ML {*