src/HOL/Tools/Quotient/quotient_term.ML

     AbsF => Const (@{const_name comp}, dummyT) $ trm1 $ trm2
   | RepF => Const (@{const_name comp}, dummyT) $ trm2 $ trm1
 
 fun get_mapfun ctxt s =
   let
-    val thy = ProofContext.theory_of ctxt
+    val thy = Proof_Context.theory_of ctxt
     val mapfun = #mapfun (Quotient_Info.maps_lookup thy s) handle Quotient_Info.NotFound =>
       raise LIFT_MATCH ("No map function for type " ^ quote s ^ " found.")
   in
     Const (mapfun, dummyT)
   end

 (* looks up the (varified) rty and qty for
    a quotient definition
 *)
 fun get_rty_qty ctxt s =
   let
-    val thy = ProofContext.theory_of ctxt
+    val thy = Proof_Context.theory_of ctxt
     val qdata = Quotient_Info.quotdata_lookup thy s handle Quotient_Info.NotFound =>
       raise LIFT_MATCH ("No quotient type " ^ quote s ^ " found.")
   in
     (#rtyp qdata, #qtyp qdata)
   end

   end
 
 (* matches a type pattern with a type *)
 fun match ctxt err ty_pat ty =
   let
-    val thy = ProofContext.theory_of ctxt
+    val thy = Proof_Context.theory_of ctxt
   in
     Sign.typ_match thy (ty_pat, ty) Vartab.empty
       handle Type.TYPE_MATCH => err ctxt ty_pat ty
   end
 

 *)
 
 (* instantiates TVars so that the term is of type ty *)
 fun force_typ ctxt trm ty =
   let
-    val thy = ProofContext.theory_of ctxt
+    val thy = Proof_Context.theory_of ctxt
     val trm_ty = fastype_of trm
     val ty_inst = Sign.typ_match thy (trm_ty, ty) Vartab.empty
   in
     map_types (Envir.subst_type ty_inst) trm
   end

 fun mk_rel_compose (trm1, trm2) =
   Const (@{const_abbrev "rel_conj"}, dummyT) $ trm1 $ trm2
 
 fun get_relmap ctxt s =
   let
-    val thy = ProofContext.theory_of ctxt
+    val thy = Proof_Context.theory_of ctxt
     val relmap = #relmap (Quotient_Info.maps_lookup thy s) handle Quotient_Info.NotFound =>
       raise LIFT_MATCH ("get_relmap (no relation map function found for type " ^ s ^ ")")
   in
     Const (relmap, dummyT)
   end

     fold_rev Term.lambda vs' (mk_relmap_aux rty)
   end
 
 fun get_equiv_rel ctxt s =
   let
-    val thy = ProofContext.theory_of ctxt
+    val thy = Proof_Context.theory_of ctxt
   in
     #equiv_rel (Quotient_Info.quotdata_lookup thy s) handle Quotient_Info.NotFound =>
       raise LIFT_MATCH ("get_quotdata (no quotient found for type " ^ s ^ ")")
   end
 

         else term_mismatch "regularize (relation mismatch)" ctxt rel rel'
       end
 
   | (_, Const _) =>
       let
-        val thy = ProofContext.theory_of ctxt
+        val thy = Proof_Context.theory_of ctxt
         fun same_const (Const (s, T)) (Const (s', T')) = (s = s') andalso matches_typ thy T T'
           | same_const _ _ = false
       in
         if same_const rtrm qtrm then rtrm
         else

 *)
 fun subst_typ ctxt ty_subst rty =
   case rty of
     Type (s, rtys) =>
       let
-        val thy = ProofContext.theory_of ctxt
+        val thy = Proof_Context.theory_of ctxt
         val rty' = Type (s, map (subst_typ ctxt ty_subst) rtys)
 
         fun matches [] = rty'
           | matches ((rty, qty)::tail) =
               case try (Sign.typ_match thy (rty, rty')) Vartab.empty of

   | Free(n, ty) => Free(n, subst_typ ctxt ty_subst ty)
   | Var(n, ty) => Var(n, subst_typ ctxt ty_subst ty)
   | Bound i => Bound i
   | Const (a, ty) =>
       let
-        val thy = ProofContext.theory_of ctxt
+        val thy = Proof_Context.theory_of ctxt
 
         fun matches [] = Const (a, subst_typ ctxt ty_subst ty)
           | matches ((rconst, qconst)::tail) =
               case try (Pattern.match thy (rconst, rtrm)) (Vartab.empty, Vartab.empty) of
                 NONE => matches tail

      true:  quotient -> raw
      false: raw -> quotient
 *)
 fun mk_ty_subst qtys direction ctxt =
   let
-    val thy = ProofContext.theory_of ctxt
+    val thy = Proof_Context.theory_of ctxt
   in
     Quotient_Info.quotdata_dest ctxt
     |> map (fn x => (#rtyp x, #qtyp x))
     |> filter (fn (_, qty) => member (Sign.typ_instance thy o swap) qtys qty)
     |> map (if direction then swap else I)