--- a/Quot/Nominal/Fv.thy	Tue Feb 23 11:22:06 2010 +0100
+++ b/Quot/Nominal/Fv.thy	Tue Feb 23 11:56:47 2010 +0100
@@ -280,7 +280,7 @@
 fun reflp_tac induct inj =
   rtac induct THEN_ALL_NEW
   asm_full_simp_tac (HOL_ss addsimps inj) THEN_ALL_NEW
-  TRY o REPEAT_ALL_NEW (CHANGED o rtac @{thm conjI}) THEN_ALL_NEW
+  TRY o REPEAT_ALL_NEW (CHANGED o rtac conjI) THEN_ALL_NEW
   (rtac @{thm exI[of _ "0 :: perm"]} THEN'
    asm_full_simp_tac (HOL_ss addsimps
      @{thms alpha_gen fresh_star_def fresh_zero_perm permute_zero ball_triv}))
@@ -290,7 +290,7 @@
 fun symp_tac induct inj eqvt =
   ((rtac @{thm impI} THEN' etac induct) ORELSE' rtac induct) THEN_ALL_NEW
   asm_full_simp_tac (HOL_ss addsimps inj) THEN_ALL_NEW
-  TRY o REPEAT_ALL_NEW (CHANGED o rtac @{thm conjI}) THEN_ALL_NEW
+  TRY o REPEAT_ALL_NEW (CHANGED o rtac conjI) THEN_ALL_NEW
   (etac @{thm alpha_gen_compose_sym} THEN' eresolve_tac eqvt)
 *}
 
@@ -323,7 +323,7 @@
   (TRY o rtac allI THEN' imp_elim_tac cases ctxt) THEN_ALL_NEW
   (
     asm_full_simp_tac (HOL_ss addsimps alpha_inj @ term_inj @ distinct) THEN'
-    TRY o REPEAT_ALL_NEW (CHANGED o rtac @{thm conjI}) THEN_ALL_NEW
+    TRY o REPEAT_ALL_NEW (CHANGED o rtac conjI) THEN_ALL_NEW
     (etac @{thm alpha_gen_compose_trans} THEN' RANGE [atac, eresolve_tac eqvt])
   )
 *}
@@ -336,9 +336,9 @@
 ML {*
 fun equivp_tac reflps symps transps =
   simp_tac (HOL_ss addsimps @{thms equivp_reflp_symp_transp reflp_def symp_def})
-  THEN' rtac @{thm conjI} THEN' rtac @{thm allI} THEN'
+  THEN' rtac conjI THEN' rtac allI THEN'
   resolve_tac reflps THEN'
-  rtac @{thm conjI} THEN' rtac @{thm allI} THEN' rtac @{thm allI} THEN'
+  rtac conjI THEN' rtac allI THEN' rtac allI THEN'
   resolve_tac symps THEN'
   rtac @{thm transp_aux} THEN' resolve_tac transps
 *}