--- a/Nominal/nominal_eqvt.ML	Tue Jul 08 11:18:31 2014 +0100
+++ b/Nominal/nominal_eqvt.ML	Thu Jul 09 02:32:46 2015 +0100
@@ -32,8 +32,7 @@
 
 fun eqvt_rel_single_case_tac ctxt pred_names pi intro =
   let
-    val thy = Proof_Context.theory_of ctxt
-    val cpi = Thm.cterm_of thy pi
+    val cpi = Thm.cterm_of ctxt pi
     val pi_intro_rule = Drule.instantiate' [] [NONE, SOME cpi] @{thm permute_boolI}
     val eqvt_sconfig = eqvt_strict_config addexcls pred_names
     val simps1 = 
@@ -48,7 +47,7 @@
         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 (prems' @ prems'' @ prems'''))
+        HEADGOAL (rtac intro THEN_ALL_NEW resolve_tac ctxt (prems' @ prems'' @ prems'''))
       end) ctxt
   end
 
@@ -92,7 +91,7 @@
 
     val (([raw_concl], [raw_pi]), ctxt') =
       ctxt
-      |> Variable.import_terms false [concl_of raw_induct']
+      |> Variable.import_terms false [Thm.concl_of raw_induct']
       ||>> Variable.variant_fixes ["p"]
     val pi = Free (raw_pi, @{typ perm})
 
@@ -108,7 +107,7 @@
   in
     Goal.prove ctxt' [] [] goal
       (fn {context, ...} => eqvt_rel_tac context pred_names pi raw_induct' intrs' 1)
-      |> Datatype_Aux.split_conj_thm
+      |> Old_Datatype_Aux.split_conj_thm
       |> Proof_Context.export ctxt' ctxt
       |> map (fn th => th RS mp)
       |> map zero_var_indexes
@@ -140,7 +139,7 @@
   end
 
 val _ =
-  Outer_Syntax.local_theory @{command_spec "equivariance"}
+  Outer_Syntax.local_theory @{command_keyword equivariance}
     "Proves equivariance for inductive predicate involving nominal datatypes."
       (Parse.const >> equivariance_cmd)