diff -r a609eea06119 -r d0ad264f8c4f Nominal/nominal_dt_alpha.ML
--- a/Nominal/nominal_dt_alpha.ML	Thu Sep 22 11:42:55 2011 +0200
+++ b/Nominal/nominal_dt_alpha.ML	Thu Nov 03 13:19:23 2011 +0000
@@ -257,7 +257,7 @@
     val alpha_raw_induct_loc = #raw_induct alpha_info;
     val alpha_intros_loc = #intrs alpha_info;
     val alpha_cases_loc = #elims alpha_info;
-    val phi = ProofContext.export_morphism lthy' lthy;
+    val phi = Proof_Context.export_morphism lthy' lthy;
     
     val all_alpha_trms = all_alpha_trms_loc
       |> map (Morphism.term phi) 
@@ -318,7 +318,7 @@
            (REPEAT_ALL_NEW (FIRST' [resolve_tac @{thms TrueI conjI}, cases_tac ctxt])))
   in
     Goal.prove ctxt' [] [] goals (fn {context, ...} => tac context)
-    |> singleton (ProofContext.export ctxt' ctxt)
+    |> singleton (Proof_Context.export ctxt' ctxt)
     |> Datatype_Aux.split_conj_thm
     |> map Datatype_Aux.split_conj_thm
     |> flat
@@ -364,7 +364,7 @@
          THEN_ALL_NEW FIRST' [rtac @{thm TrueI}, cases_tac ctxt])
   in
     Goal.prove ctxt' [] [] goals (fn {context, ...} => tac context)
-    |> singleton (ProofContext.export ctxt' ctxt)
+    |> singleton (Proof_Context.export ctxt' ctxt)
     |> Datatype_Aux.split_conj_thm
     |> map (fn th => th RS mp) 
     |> map Datatype_Aux.split_conj_thm
@@ -830,7 +830,7 @@
   in
     alpha_prove (alpha_trms @ alpha_bn_trms) goals alpha_raw_induct 
       (raw_prove_perm_bn_tac alpha_result simps) ctxt
-     |> ProofContext.export ctxt' ctxt
+     |> Proof_Context.export ctxt' ctxt
      |> map atomize
      |> map single
      |> map (curry (op OF) perm_bn_rsp)