diff -r 4af8a92396ce -r a44479bde681 Nominal/nominal_thmdecls.ML
--- a/Nominal/nominal_thmdecls.ML	Mon Jul 20 11:21:59 2015 +0100
+++ b/Nominal/nominal_thmdecls.ML	Tue Mar 22 12:18:30 2016 +0000
@@ -183,8 +183,9 @@
   in
     REPEAT o FIRST'
       [CHANGED o simp_tac (put_simpset HOL_basic_ss ctxt addsimps ss_thms),
-       rtac (thm RS @{thm "trans"}),
-       rtac @{thm "trans"[OF "permute_fun_def"]} THEN' rtac @{thm "ext"}]
+       resolve_tac ctxt [thm RS @{thm trans}],
+       resolve_tac ctxt @{thms trans[OF "permute_fun_def"]} THEN'
+       resolve_tac ctxt @{thms ext}]
   end
 
 in
@@ -213,8 +214,12 @@
   let
     val ss_thms = @{thms "permute_minus_cancel"(2)}
   in
-    EVERY' [rtac @{thm "iffI"}, dtac @{thm "permute_boolE"}, rtac thm, assume_tac ctxt,
-      rtac @{thm "permute_boolI"}, dtac thm', 
+    EVERY' [resolve_tac ctxt @{thms iffI},
+      dresolve_tac ctxt @{thms permute_boolE},
+      resolve_tac ctxt [thm],
+      assume_tac ctxt,
+      resolve_tac ctxt @{thms permute_boolI},
+      dresolve_tac ctxt [thm'],
       full_simp_tac (put_simpset HOL_basic_ss ctxt addsimps ss_thms)]
   end
 
@@ -232,7 +237,7 @@
     val p = concl |> dest_comb |> snd |> find_perm
     val goal = HOLogic.mk_Trueprop (HOLogic.mk_eq (mk_perm p prem, concl))
     val ([goal', p'], ctxt') = Variable.import_terms false [goal, p] ctxt
-    val thm' = Drule.cterm_instantiate [apply2 (Thm.cterm_of ctxt') (p, mk_minus p')] thm
+    val thm' = infer_instantiate ctxt' [(#1 (dest_Var p), Thm.cterm_of ctxt' (mk_minus p'))] thm
   in
     Goal.prove ctxt' [] [] goal' (fn {context = ctxt'', ...} => tac ctxt'' thm thm' 1)
       |> singleton (Proof_Context.export ctxt' ctxt)