diff -r a609eea06119 -r d0ad264f8c4f Nominal/nominal_dt_rawfuns.ML
--- a/Nominal/nominal_dt_rawfuns.ML	Thu Sep 22 11:42:55 2011 +0200
+++ b/Nominal/nominal_dt_rawfuns.ML	Thu Nov 03 13:19:23 2011 +0000
@@ -261,7 +261,7 @@
  
     val {fs, simps, inducts, ...} = info; 
 
-    val morphism = ProofContext.export_morphism lthy'' lthy
+    val morphism = Proof_Context.export_morphism lthy'' lthy
     val simps_exp = map (Morphism.thm morphism) (the simps)
     val inducts_exp = map (Morphism.thm morphism) (the inducts)
     
@@ -334,7 +334,7 @@
 
       val {fs, simps, ...} = info;
 
-      val morphism = ProofContext.export_morphism lthy'' lthy
+      val morphism = Proof_Context.export_morphism lthy'' lthy
       val simps_exp = map (Morphism.thm morphism) (the simps)
     in
       (fs, simps_exp, lthy'')
@@ -467,7 +467,7 @@
 fun prove_eqvt_tac insts ind_thms const_names simps ctxt = 
   HEADGOAL
     (Object_Logic.full_atomize_tac
-     THEN' (DETERM o (InductTacs.induct_rules_tac ctxt insts ind_thms))  
+     THEN' (DETERM o (Induct_Tacs.induct_rules_tac ctxt insts ind_thms))  
      THEN_ALL_NEW  subproof_tac const_names simps ctxt)
 
 fun mk_eqvt_goal pi const arg =
@@ -498,7 +498,7 @@
     in
       Goal.prove_multi ctxt'' [] [] goals (fn {context, ...} => 
         prove_eqvt_tac insts ind_thms const_names simps context)
-      |> ProofContext.export ctxt'' ctxt
+      |> Proof_Context.export ctxt'' ctxt
     end