src/HOL/Nominal/nominal_induct.ML

         (x, tuple (map Free avoiding)) ::
         map_filter (fn (z, SOME t) => SOME (z, t) | _ => NONE) (zs ~~ inst)
       end;
      val substs =
        map2 subst insts concls |> flat |> distinct (op =)
-       |> map (pairself (Thm.cterm_of (ProofContext.theory_of ctxt)));
+       |> map (pairself (Thm.cterm_of (Proof_Context.theory_of ctxt)));
   in 
     (((cases, nconcls), consumes), Drule.cterm_instantiate substs joined_rule) 
   end;
 
 fun rename_params_rule internal xs rule =

 
 (* nominal_induct_tac *)
 
 fun nominal_induct_tac ctxt simp def_insts avoiding fixings rules facts =
   let
-    val thy = ProofContext.theory_of ctxt;
+    val thy = Proof_Context.theory_of ctxt;
     val cert = Thm.cterm_of thy;
 
     val ((insts, defs), defs_ctxt) = fold_map Induct.add_defs def_insts ctxt |>> split_list;
     val atomized_defs = map (map (Conv.fconv_rule Induct.atomize_cterm)) defs;
 
     val finish_rule =
       split_all_tuples
       #> rename_params_rule true
-        (map (Name.clean o ProofContext.revert_skolem defs_ctxt o fst) avoiding);
+        (map (Name.clean o Proof_Context.revert_skolem defs_ctxt o fst) avoiding);
 
     fun rule_cases ctxt r =
       let val r' = if simp then Induct.simplified_rule ctxt r else r
       in Rule_Cases.make_nested (Thm.prop_of r') (Induct.rulified_term r') end;
   in

             Induct.guess_instance ctxt
               (finish_rule (Induct.internalize more_consumes rule)) i st'
             |> Seq.maps (fn rule' =>
               CASES (rule_cases ctxt rule' cases)
                 (Tactic.rtac (rename_params_rule false [] rule') i THEN
-                  PRIMITIVE (singleton (ProofContext.export defs_ctxt ctxt))) st'))))
+                  PRIMITIVE (singleton (Proof_Context.export defs_ctxt ctxt))) st'))))
     THEN_ALL_NEW_CASES
       ((if simp then Induct.simplify_tac ctxt THEN' (TRY o Induct.trivial_tac)
         else K all_tac)
        THEN_ALL_NEW Induct.rulify_tac)
   end;