diff -r 4af8a92396ce -r c4f31f1564b7 Nominal/nominal_eqvt.ML
--- a/Nominal/nominal_eqvt.ML	Mon Jul 20 11:21:59 2015 +0100
+++ b/Nominal/nominal_eqvt.ML	Sat Mar 19 21:06:48 2016 +0000
@@ -33,7 +33,7 @@
 fun eqvt_rel_single_case_tac ctxt pred_names pi intro =
   let
     val cpi = Thm.cterm_of ctxt pi
-    val pi_intro_rule = Drule.instantiate' [] [NONE, SOME cpi] @{thm permute_boolI}
+    val pi_intro_rule = Thm.instantiate' [] [NONE, SOME cpi] @{thm permute_boolI}
     val eqvt_sconfig = eqvt_strict_config addexcls pred_names
     val simps1 = 
       put_simpset HOL_basic_ss ctxt addsimps @{thms permute_fun_def permute_self split_paired_all}
@@ -47,7 +47,8 @@
         val prems'' = map (fn thm => eqvt_rule ctxt eqvt_sconfig (thm RS pi_intro_rule)) prems'
         val prems''' = map (simplify simps2 o simplify simps1) prems''
       in
-        HEADGOAL (rtac intro THEN_ALL_NEW resolve_tac ctxt (prems' @ prems'' @ prems'''))
+        HEADGOAL (resolve_tac ctxt [intro] THEN_ALL_NEW
+          resolve_tac ctxt (prems' @ prems'' @ prems'''))
       end) ctxt
   end
 
@@ -55,7 +56,7 @@
   let
     val cases = map (eqvt_rel_single_case_tac ctxt pred_names pi) intros
   in
-    EVERY' ((DETERM o rtac induct) :: cases)
+    EVERY' ((DETERM o resolve_tac ctxt [induct]) :: cases)
   end