src/HOL/Nominal/nominal_thmdecls.ML

   then tac THEN' (K (print_tac ("after " ^ msg)))
   else tac
 
 fun prove_eqvt_tac ctxt orig_thm pi pi' =
   let
-    val thy = ProofContext.theory_of ctxt
+    val thy = Proof_Context.theory_of ctxt
     val mypi = Thm.cterm_of thy pi
     val T = fastype_of pi'
     val mypifree = Thm.cterm_of thy (Const (@{const_name "rev"}, T --> T) $ pi')
     val perm_pi_simp = Global_Theory.get_thms thy "perm_pi_simp"
   in

                        full_simp_tac (HOL_basic_ss addsimps perm_pi_simp))]
   end;
 
 fun get_derived_thm ctxt hyp concl orig_thm pi typi =
   let
-    val thy = ProofContext.theory_of ctxt;
+    val thy = Proof_Context.theory_of ctxt;
     val pi' = Var (pi, typi);
     val lhs = Const (@{const_name "perm"}, typi --> HOLogic.boolT --> HOLogic.boolT) $ pi' $ hyp;
     val ([goal_term, pi''], ctxt') = Variable.import_terms false
       [HOLogic.mk_Trueprop (HOLogic.mk_eq (lhs, concl)), pi'] ctxt
     val _ = writeln (Syntax.string_of_term ctxt' goal_term);
   in
     Goal.prove ctxt' [] [] goal_term
       (fn _ => prove_eqvt_tac ctxt' orig_thm pi' pi'') |>
-    singleton (ProofContext.export ctxt' ctxt)
+    singleton (Proof_Context.export ctxt' ctxt)
   end
 
 (* replaces in t every variable, say x, with pi o x *)
 fun apply_pi trm (pi, typi) =
 let