src/HOL/Tools/Nitpick/nitpick_hol.ML

   Same.commit (Envir.subst_type_same
                    (Sign.typ_match thy (T1, T1') Vartab.empty)) T2
   handle Type.TYPE_MATCH =>
          raise TYPE ("Nitpick_HOL.instantiate_type", [T1, T1'], [])
 fun varify_and_instantiate_type ctxt T1 T1' T2 =
-  let val thy = ProofContext.theory_of ctxt in
+  let val thy = Proof_Context.theory_of ctxt in
     instantiate_type thy (varify_type ctxt T1) T1' (varify_type ctxt T2)
   end
 
 fun repair_constr_type ctxt body_T' T =
   varify_and_instantiate_type ctxt (body_type T) body_T' T

   | is_codatatype _ _ = false
 fun is_real_quot_type thy (Type (s, _)) =
     is_some (Quotient_Info.quotdata_lookup_raw thy s)
   | is_real_quot_type _ _ = false
 fun is_quot_type ctxt T =
-  let val thy = ProofContext.theory_of ctxt in
+  let val thy = Proof_Context.theory_of ctxt in
     is_real_quot_type thy T andalso not (is_codatatype ctxt T)
   end
 fun is_pure_typedef ctxt (T as Type (s, _)) =
-    let val thy = ProofContext.theory_of ctxt in
+    let val thy = Proof_Context.theory_of ctxt in
       is_typedef ctxt s andalso
       not (is_real_datatype thy s orelse is_real_quot_type thy T orelse
            is_codatatype ctxt T orelse is_record_type T orelse
            is_integer_like_type T)
     end

          | _ => false
        end
      | NONE => false)
   | is_univ_typedef _ _ = false
 fun is_datatype ctxt stds (T as Type (s, _)) =
-    let val thy = ProofContext.theory_of ctxt in
+    let val thy = Proof_Context.theory_of ctxt in
       (is_typedef ctxt s orelse is_codatatype ctxt T orelse
        T = @{typ ind} orelse is_real_quot_type thy T) andalso
       not (is_basic_datatype thy stds s)
     end
   | is_datatype _ _ _ = false

 fun is_constr_like ctxt (s, T) =
   member (op =) [@{const_name FunBox}, @{const_name PairBox},
                  @{const_name Quot}, @{const_name Zero_Rep},
                  @{const_name Suc_Rep}] s orelse
   let
-    val thy = ProofContext.theory_of ctxt
+    val thy = Proof_Context.theory_of ctxt
     val (x as (_, T)) = (s, unarize_unbox_etc_type T)
   in
     is_real_constr thy x orelse is_record_constr x orelse
     (is_abs_fun ctxt x andalso is_pure_typedef ctxt (range_type T)) orelse
     is_coconstr ctxt x
   end
 fun is_stale_constr ctxt (x as (_, T)) =
   is_codatatype ctxt (body_type T) andalso is_constr_like ctxt x andalso
   not (is_coconstr ctxt x)
 fun is_constr ctxt stds (x as (_, T)) =
-  let val thy = ProofContext.theory_of ctxt in
+  let val thy = Proof_Context.theory_of ctxt in
     is_constr_like ctxt x andalso
     not (is_basic_datatype thy stds
                          (fst (dest_Type (unarize_type (body_type T))))) andalso
     not (is_stale_constr ctxt x)
   end

         val m = fold (Integer.add o num_factors_in_type)
                      (List.take (arg_Ts, n)) 0
       in Abs ("x", dataT, aux m (nth arg_Ts n) |> snd) end
   end
 fun select_nth_constr_arg ctxt stds x t n res_T =
-  let val thy = ProofContext.theory_of ctxt in
+  let val thy = Proof_Context.theory_of ctxt in
     (case strip_comb t of
        (Const x', args) =>
        if x = x' then nth args n
        else if is_constr_like ctxt x' then Const (@{const_name unknown}, res_T)
        else raise SAME ()

       | do_eq _ = false
   in do_eq end
 
 fun all_axioms_of ctxt subst =
   let
-    val thy = ProofContext.theory_of ctxt
+    val thy = Proof_Context.theory_of ctxt
     val axioms_of_thys =
       maps Thm.axioms_of
       #> map (apsnd (subst_atomic subst o prop_of))
       #> filter_out (is_class_axiom o snd)
     val specs = Defs.all_specifications_of (Theory.defs_of thy)

                     end
                  | NONE => t)
                | t => t)
 
 fun case_const_names ctxt stds =
-  let val thy = ProofContext.theory_of ctxt in
+  let val thy = Proof_Context.theory_of ctxt in
     Symtab.fold (fn (dtype_s, {index, descr, case_name, ...}) =>
                     if is_basic_datatype thy stds dtype_s then
                       I
                     else
                       cons (case_name, AList.lookup (op =) descr index

 fun const_choice_spec_table ctxt subst =
   map (subst_atomic subst o prop_of) (Nitpick_Choice_Specs.get ctxt)
   |> const_nondef_table
 
 fun inductive_intro_table ctxt subst def_tables =
-  let val thy = ProofContext.theory_of ctxt in
+  let val thy = Proof_Context.theory_of ctxt in
     def_table_for
         (maps (map (unfold_mutually_inductive_preds thy def_tables o prop_of)
                o snd o snd)
          o filter (fn (cat, _) => cat = Spec_Rules.Inductive orelse
                                   cat = Spec_Rules.Co_Inductive)

   Unsynchronized.change simp_table
       (Symtab.update (s, eqs @ these (Symtab.lookup (!simp_table) s)))
 
 fun inverse_axioms_for_rep_fun ctxt (x as (_, T)) =
   let
-    val thy = ProofContext.theory_of ctxt
+    val thy = Proof_Context.theory_of ctxt
     val abs_T = domain_type T
   in
     typedef_info ctxt (fst (dest_Type abs_T)) |> the
     |> pairf #Abs_inverse #Rep_inverse
     |> pairself (specialize_type thy x o prop_of o the)
     ||> single |> op ::
   end
 fun optimized_typedef_axioms ctxt (abs_z as (abs_s, _)) =
   let
-    val thy = ProofContext.theory_of ctxt
+    val thy = Proof_Context.theory_of ctxt
     val abs_T = Type abs_z
   in
     if is_univ_typedef ctxt abs_T then
       []
     else case typedef_info ctxt abs_s of

       end
     | NONE => []
   end
 fun optimized_quot_type_axioms ctxt stds abs_z =
   let
-    val thy = ProofContext.theory_of ctxt
+    val thy = Proof_Context.theory_of ctxt
     val abs_T = Type abs_z
     val rep_T = rep_type_for_quot_type thy abs_T
     val (equiv_rel, partial) = equiv_relation_for_quot_type thy abs_T
     val a_var = Var (("a", 0), abs_T)
     val x_var = Var (("x", 0), rep_T)