src/HOL/Tools/Quotient/quotient_tacs.ML

    we rely on unification/instantiation to check whether the
    theorem applies and return NONE if it doesn't.
 *)
 fun calculate_inst ctxt ball_bex_thm redex R1 R2 =
   let
-    val thy = ProofContext.theory_of ctxt
+    val thy = Proof_Context.theory_of ctxt
     fun get_lhs thm = fst (Logic.dest_equals (Thm.concl_of thm))
     val ty_inst = map (SOME o ctyp_of thy) [domain_type (fastype_of R2)]
     val trm_inst = map (SOME o cterm_of thy) [R2, R1]
   in
     (case try (Drule.instantiate' ty_inst trm_inst) ball_bex_thm of

 
 fun eq_imp_rel_get ctxt = map (OF1 eq_imp_rel) (Quotient_Info.equiv_rules_get ctxt)
 
 fun regularize_tac ctxt =
   let
-    val thy = ProofContext.theory_of ctxt
+    val thy = Proof_Context.theory_of ctxt
     val ball_pat = @{term "Ball (Respects (R1 ===> R2)) P"}
     val bex_pat = @{term "Bex (Respects (R1 ===> R2)) P"}
     val simproc =
       Simplifier.simproc_global_i thy "" [ball_pat, bex_pat] (K (ball_bex_range_simproc))
     val simpset =

 fun quot_true_simple_conv ctxt fnctn ctrm =
   case term_of ctrm of
     (Const (@{const_name Quot_True}, _) $ x) =>
       let
         val fx = fnctn x;
-        val thy = ProofContext.theory_of ctxt;
+        val thy = Proof_Context.theory_of ctxt;
         val cx = cterm_of thy x;
         val cfx = cterm_of thy fx;
         val cxt = ctyp_of thy (fastype_of x);
         val cfxt = ctyp_of thy (fastype_of fx);
         val thm = Drule.instantiate' [SOME cxt, SOME cfxt] [SOME cx, SOME cfx] @{thm QT_imp}

           else
             let
               val ty_x = fastype_of x
               val ty_b = fastype_of qt_arg
               val ty_f = range_type (fastype_of f)
-              val thy = ProofContext.theory_of context
+              val thy = Proof_Context.theory_of context
               val ty_inst = map (SOME o (ctyp_of thy)) [ty_x, ty_b, ty_f]
               val t_inst = map (SOME o (cterm_of thy)) [R2, f, g, x, y];
               val inst_thm = Drule.instantiate' ty_inst
                 ([NONE, NONE, NONE] @ t_inst) @{thm apply_rsp}
             in

 (* Instantiates and applies 'equals_rsp'. Since the theorem is
    complex we rely on instantiation to tell us if it applies
 *)
 fun equals_rsp_tac R ctxt =
   let
-    val thy = ProofContext.theory_of ctxt
+    val thy = Proof_Context.theory_of ctxt
   in
     case try (cterm_of thy) R of (* There can be loose bounds in R *)
       SOME ctm =>
         let
           val ty = domain_type (fastype_of R)

   SUBGOAL (fn (goal, i) =>
     (case try bare_concl goal of
       SOME (rel $ _ $ (rep $ (Bound _ $ _))) => no_tac
     | SOME (rel $ _ $ (rep $ (abs $ _))) =>
         let
-          val thy = ProofContext.theory_of ctxt;
+          val thy = Proof_Context.theory_of ctxt;
           val (ty_a, ty_b) = dest_funT (fastype_of abs);
           val ty_inst = map (SOME o (ctyp_of thy)) [ty_a, ty_b];
         in
           case try (map (SOME o (cterm_of thy))) [rel, abs, rep] of
             SOME t_inst =>

 *)
 fun lambda_prs_simple_conv ctxt ctrm =
   (case term_of ctrm of
     (Const (@{const_name map_fun}, _) $ r1 $ a2) $ (Abs _) =>
       let
-        val thy = ProofContext.theory_of ctxt
+        val thy = Proof_Context.theory_of ctxt
         val (ty_b, ty_a) = dest_funT (fastype_of r1)
         val (ty_c, ty_d) = dest_funT (fastype_of a2)
         val tyinst = map (SOME o (ctyp_of thy)) [ty_a, ty_b, ty_c, ty_d]
         val tinst = [NONE, NONE, SOME (cterm_of thy r1), NONE, SOME (cterm_of thy a2)]
         val thm1 = Drule.instantiate' tyinst tinst @{thm lambda_prs[THEN eq_reflection]}

   HOLogic.dest_Trueprop #> f #> HOLogic.mk_Trueprop
 
 fun gen_frees_tac ctxt =
   SUBGOAL (fn (concl, i) =>
     let
-      val thy = ProofContext.theory_of ctxt
+      val thy = Proof_Context.theory_of ctxt
       val vrs = Term.add_frees concl []
       val cvrs = map (cterm_of thy o Free) vrs
       val concl' = apply_under_Trueprop (all_list vrs) concl
       val goal = Logic.mk_implies (concl', concl)
       val rule = Goal.prove ctxt [] [] goal

     error msg
   end
 
 fun procedure_inst ctxt rtrm qtrm =
   let
-    val thy = ProofContext.theory_of ctxt
+    val thy = Proof_Context.theory_of ctxt
     val rtrm' = HOLogic.dest_Trueprop rtrm
     val qtrm' = HOLogic.dest_Trueprop qtrm
     val reg_goal = Quotient_Term.regularize_trm_chk ctxt (rtrm', qtrm')
       handle Quotient_Term.LIFT_MATCH msg => lift_match_error ctxt msg rtrm qtrm
     val inj_goal = Quotient_Term.inj_repabs_trm_chk ctxt (reg_goal, qtrm')

     val ((_, [rthm']), ctxt') = Variable.import true [rthm] ctxt
     val goal = Quotient_Term.derive_qtrm ctxt' qtys (prop_of rthm')
   in
     Goal.prove ctxt' [] [] goal
       (K (HEADGOAL (lift_single_tac ctxt' simps rthm')))
-    |> singleton (ProofContext.export ctxt' ctxt)
+    |> singleton (Proof_Context.export ctxt' ctxt)
   end
 
 
 (* lifting as an attribute *)