diff -r a609eea06119 -r d0ad264f8c4f Nominal/nominal_thmdecls.ML
--- a/Nominal/nominal_thmdecls.ML	Thu Sep 22 11:42:55 2011 +0200
+++ b/Nominal/nominal_thmdecls.ML	Thu Nov 03 13:19:23 2011 +0000
@@ -156,7 +156,7 @@
         val ([goal', p'], ctxt') = Variable.import_terms false [goal, p] ctxt
       in
         Goal.prove ctxt [] [] goal' (fn _ => eqvt_transform_eq_tac thm 1)
-        |> singleton (ProofContext.export ctxt' ctxt)
+        |> singleton (Proof_Context.export ctxt' ctxt)
         |> safe_mk_equiv
         |> zero_var_indexes
       end
@@ -167,7 +167,7 @@
 
 fun eqvt_transform_imp_tac ctxt p p' thm = 
   let
-    val thy = ProofContext.theory_of ctxt
+    val thy = Proof_Context.theory_of ctxt
     val cp = Thm.cterm_of thy p
     val cp' = Thm.cterm_of thy (mk_minus p')
     val thm' = Drule.cterm_instantiate [(cp, cp')] thm
@@ -199,7 +199,7 @@
       in
         Goal.prove ctxt' [] [] goal'
           (fn _ => eqvt_transform_imp_tac ctxt' (the p) p' thm 1) 
-        |> singleton (ProofContext.export ctxt' ctxt)
+        |> singleton (Proof_Context.export ctxt' ctxt)
       end
   end