diff -r a609eea06119 -r d0ad264f8c4f Nominal/nominal_mutual.ML
--- a/Nominal/nominal_mutual.ML	Thu Sep 22 11:42:55 2011 +0200
+++ b/Nominal/nominal_mutual.ML	Thu Nov 03 13:19:23 2011 +0000
@@ -157,7 +157,7 @@
 
 fun in_context ctxt (f, pre_qs, pre_gs, pre_args, pre_rhs) F =
   let
-    val thy = ProofContext.theory_of ctxt
+    val thy = Proof_Context.theory_of ctxt
 
     val oqnames = map fst pre_qs
     val (qs, _) = Variable.variant_fixes oqnames ctxt
@@ -229,14 +229,14 @@
     Goal.prove ctxt' [] [] (HOLogic.Trueprop $ HOLogic.mk_eq (goal_lhs, goal_rhs))
       (fn _ => (Local_Defs.unfold_tac ctxt all_orig_fdefs)
          THEN (asm_full_simp_tac ss 1))
-    |> singleton (ProofContext.export ctxt' ctxt)
+    |> singleton (Proof_Context.export ctxt' ctxt)
     |> restore_cond
     |> export
   end
 
 fun mk_applied_form ctxt caTs thm =
   let
-    val thy = ProofContext.theory_of ctxt
+    val thy = Proof_Context.theory_of ctxt
     val xs = map_index (fn (i,T) => cterm_of thy (Free ("x" ^ string_of_int i, T))) caTs (* FIXME: Bind xs properly *)
   in
     fold (fn x => fn thm => Thm.combination thm (Thm.reflexive x)) xs thm
@@ -247,7 +247,7 @@
 
 fun mutual_induct_rules lthy induct all_f_defs (Mutual {n, ST, parts, ...}) =
   let
-    val cert = cterm_of (ProofContext.theory_of lthy)
+    val cert = cterm_of (Proof_Context.theory_of lthy)
     val newPs =
       map2 (fn Pname => fn MutualPart {cargTs, ...} =>
           Free (Pname, cargTs ---> HOLogic.boolT))
@@ -340,7 +340,7 @@
   in
     Goal.prove ctxt' (flat arg_namess) [] goal
       (fn {context, ...} => HEADGOAL (DETERM o (rtac induct_thm) THEN' RANGE (map tac eqvts_thms)))
-    |> singleton (ProofContext.export ctxt' ctxt)
+    |> singleton (Proof_Context.export ctxt' ctxt)
     |> split_conj_thm
     |> map (fn th => th RS mp)
   end