--- a/Nominal/nominal_inductive.ML	Thu Sep 22 11:42:55 2011 +0200
+++ b/Nominal/nominal_inductive.ML	Thu Nov 03 13:19:23 2011 +0000
@@ -170,7 +170,7 @@
 fun non_binder_tac prem intr_cvars Ps ctxt = 
   Subgoal.SUBPROOF (fn {context, params, prems, ...} =>
     let
-      val thy = ProofContext.theory_of context
+      val thy = Proof_Context.theory_of context
       val (prms, p, _) = split_last2 (map snd params)
       val prm_tys = map (fastype_of o term_of) prms
       val cperms = map (cterm_of thy o perm_const) prm_tys
@@ -223,7 +223,7 @@
 fun binder_tac prem intr_cvars param_trms Ps user_thm avoid_trm concl_args ctxt = 
   Subgoal.FOCUS (fn {context = ctxt, params, prems, concl, ...} =>
     let
-      val thy = ProofContext.theory_of ctxt
+      val thy = Proof_Context.theory_of ctxt
       val (prms, p, c) = split_last2 (map snd params)
       val prm_trms = map term_of prms
       val prm_tys = map fastype_of prm_trms
@@ -273,7 +273,7 @@
                     eqvt_stac context,
                     rtac prem',
                     RANGE (tac_fresh :: map (SUBGOAL o select) prems) ])
-        |> singleton (ProofContext.export ctxt' ctxt)        
+        |> singleton (Proof_Context.export ctxt' ctxt)        
     in
       rtac side_thm 1
     end) ctxt
@@ -300,7 +300,7 @@
 
 fun prove_strong_inductive pred_names rule_names avoids raw_induct intrs ctxt =
   let
-    val thy = ProofContext.theory_of ctxt
+    val thy = Proof_Context.theory_of ctxt
     val ((_, [raw_induct']), ctxt') = Variable.import true [raw_induct] ctxt
 
     val (ind_prems, ind_concl) = raw_induct'
@@ -357,7 +357,7 @@
       let
         val strong_ind_thms = Goal.prove ctxt [] ind_prems' ind_concl' 
         (prove_sinduct_tac raw_induct user_thms Ps avoids avoid_trms intr_cvars param_trms intr_concls_args) 
-          |> singleton (ProofContext.export ctxt ctxt_outside)
+          |> singleton (Proof_Context.export ctxt ctxt_outside)
           |> Datatype_Aux.split_conj_thm
           |> map (fn thm => thm RS normalise)
           |> map (asm_full_simplify (HOL_basic_ss addsimps @{thms permute_zero induct_rulify})) 
@@ -383,7 +383,7 @@
 
 fun prove_strong_inductive_cmd (pred_name, avoids) ctxt =
   let
-    val thy = ProofContext.theory_of ctxt;
+    val thy = Proof_Context.theory_of ctxt;
     val ({names, ...}, {raw_induct, intrs, ...}) =
       Inductive.the_inductive ctxt (Sign.intern_const thy pred_name);