--- a/Nominal/nominal_eqvt.ML	Thu Sep 22 11:42:55 2011 +0200
+++ b/Nominal/nominal_eqvt.ML	Thu Nov 03 13:19:23 2011 +0000
@@ -32,7 +32,7 @@
 
 fun eqvt_rel_single_case_tac ctxt pred_names pi intro  = 
   let
-    val thy = ProofContext.theory_of ctxt
+    val thy = Proof_Context.theory_of ctxt
     val cpi = Thm.cterm_of thy (mk_minus pi)
     val pi_intro_rule = Drule.instantiate' [] [SOME cpi] perm_boolE
     val simps1 = HOL_basic_ss addsimps @{thms permute_fun_def minus_minus split_paired_all}
@@ -104,7 +104,7 @@
     Goal.prove ctxt' [] [] goal 
       (fn {context,...} => eqvt_rel_tac context pred_names pi raw_induct' intrs' 1)
       |> Datatype_Aux.split_conj_thm 
-      |> ProofContext.export ctxt' ctxt
+      |> Proof_Context.export ctxt' ctxt
       |> map (fn th => th RS mp)
       |> map zero_var_indexes
   end
@@ -122,7 +122,7 @@
 
 fun equivariance_cmd pred_name ctxt =
   let
-    val thy = ProofContext.theory_of ctxt
+    val thy = Proof_Context.theory_of ctxt
     val ({names, ...}, {preds, raw_induct, intrs, ...}) =
       Inductive.the_inductive ctxt (Sign.intern_const thy pred_name)
     val thms = raw_equivariance preds raw_induct intrs ctxt