# HG changeset patch
# User wenzelm
# Date 1587500399 -7200
# Node ID 3875815f59677fc7a62589b1ae135b71f908fbc5
# Parent  5ef7f374e0f8bb0609cd0261edc905da513d0832
clarified signature: avoid clash with Isabelle/Scala Term.OFCLASS on case-insensible file-system;

diff -r 5ef7f374e0f8 -r 3875815f5967 src/Doc/Implementation/Logic.thy
--- a/src/Doc/Implementation/Logic.thy	Tue Apr 21 22:04:15 2020 +0200
+++ b/src/Doc/Implementation/Logic.thy	Tue Apr 21 22:19:59 2020 +0200
@@ -1200,7 +1200,7 @@
   constructors @{index_ML Abst}, @{index_ML AbsP}, @{index_ML_op "%"},
   @{index_ML_op "%%"}, @{index_ML PBound}, @{index_ML MinProof}, @{index_ML
   Hyp}, @{index_ML PAxm}, @{index_ML Oracle}, @{index_ML PThm} as explained
-  above. %FIXME OfClass (!?)
+  above. %FIXME PClass (!?)
 
   \<^descr> Type \<^ML_type>\<open>proof_body\<close> represents the nested proof information of a
   named theorem, consisting of a digest of oracles and named theorem over some
diff -r 5ef7f374e0f8 -r 3875815f5967 src/HOL/Tools/rewrite_hol_proof.ML
--- a/src/HOL/Tools/rewrite_hol_proof.ML	Tue Apr 21 22:04:15 2020 +0200
+++ b/src/HOL/Tools/rewrite_hol_proof.ML	Tue Apr 21 22:19:59 2020 +0200
@@ -34,9 +34,9 @@
    \<open>(meta_eq_to_obj_eq \<cdot> TYPE('U) \<cdot> x1 \<cdot> x2 \<bullet> prfU \<bullet>
       (combination \<cdot> TYPE('T) \<cdot> TYPE('U) \<cdot> f \<cdot> g \<cdot> x \<cdot> y \<bullet> prf1 \<bullet> prf2)) \<equiv>
     (cong \<cdot> TYPE('T) \<cdot> TYPE('U) \<cdot> f \<cdot> g \<cdot> x \<cdot> y \<bullet>
-      (Pure.OfClass type_class \<cdot> TYPE('T)) \<bullet> prfU \<bullet>
-      (meta_eq_to_obj_eq \<cdot> TYPE('T \<Rightarrow> 'U) \<cdot> f \<cdot> g \<bullet> (Pure.OfClass type_class \<cdot> TYPE('T \<Rightarrow> 'U)) \<bullet> prf1) \<bullet>
-      (meta_eq_to_obj_eq \<cdot> TYPE('T) \<cdot> x \<cdot> y \<bullet> (Pure.OfClass type_class \<cdot> TYPE('T)) \<bullet> prf2))\<close>,
+      (Pure.PClass type_class \<cdot> TYPE('T)) \<bullet> prfU \<bullet>
+      (meta_eq_to_obj_eq \<cdot> TYPE('T \<Rightarrow> 'U) \<cdot> f \<cdot> g \<bullet> (Pure.PClass type_class \<cdot> TYPE('T \<Rightarrow> 'U)) \<bullet> prf1) \<bullet>
+      (meta_eq_to_obj_eq \<cdot> TYPE('T) \<cdot> x \<cdot> y \<bullet> (Pure.PClass type_class \<cdot> TYPE('T)) \<bullet> prf2))\<close>,
 
    \<open>(meta_eq_to_obj_eq \<cdot> TYPE('T) \<cdot> x1 \<cdot> x2 \<bullet> prfT \<bullet>
       (axm.transitive \<cdot> TYPE('T) \<cdot> x \<cdot> y \<cdot> z \<bullet> prf1 \<bullet> prf2)) \<equiv>
@@ -54,9 +54,9 @@
    \<open>(meta_eq_to_obj_eq \<cdot> TYPE('T \<Rightarrow> 'U) \<cdot> x1 \<cdot> x2 \<bullet> prfTU \<bullet>
       (abstract_rule \<cdot> TYPE('T) \<cdot> TYPE('U) \<cdot> f \<cdot> g \<bullet> prf)) \<equiv>
     (ext \<cdot> TYPE('T) \<cdot> TYPE('U) \<cdot> f \<cdot> g \<bullet>
-      (Pure.OfClass type_class \<cdot> TYPE('T)) \<bullet> (Pure.OfClass type_class \<cdot> TYPE('U)) \<bullet>
+      (Pure.PClass type_class \<cdot> TYPE('T)) \<bullet> (Pure.PClass type_class \<cdot> TYPE('U)) \<bullet>
       (\<^bold>\<lambda>(x::'T). meta_eq_to_obj_eq \<cdot> TYPE('U) \<cdot> f x \<cdot> g x \<bullet>
-         (Pure.OfClass type_class \<cdot> TYPE('U)) \<bullet> (prf \<cdot> x)))\<close>,
+         (Pure.PClass type_class \<cdot> TYPE('U)) \<bullet> (prf \<cdot> x)))\<close>,
 
    \<open>(meta_eq_to_obj_eq \<cdot> TYPE('T) \<cdot> x \<cdot> y \<bullet> prfT \<bullet>
       (eq_reflection \<cdot> TYPE('T) \<cdot> x \<cdot> y \<bullet> prfT \<bullet> prf)) \<equiv> prf\<close>,
@@ -70,9 +70,9 @@
         prfT \<bullet> arity_type_bool \<bullet>
         (cong \<cdot> TYPE('T) \<cdot> TYPE('T\<Rightarrow>bool) \<cdot>
           ((=) :: 'T\<Rightarrow>'T\<Rightarrow>bool) \<cdot> ((=) :: 'T\<Rightarrow>'T\<Rightarrow>bool) \<cdot> A \<cdot> B \<bullet>
-          prfT \<bullet> (Pure.OfClass type_class \<cdot> TYPE('T\<Rightarrow>bool)) \<bullet>
+          prfT \<bullet> (Pure.PClass type_class \<cdot> TYPE('T\<Rightarrow>bool)) \<bullet>
           (HOL.refl \<cdot> TYPE('T\<Rightarrow>'T\<Rightarrow>bool) \<cdot> ((=) :: 'T\<Rightarrow>'T\<Rightarrow>bool) \<bullet>
-             (Pure.OfClass type_class \<cdot> TYPE('T\<Rightarrow>'T\<Rightarrow>bool))) \<bullet>
+             (Pure.PClass type_class \<cdot> TYPE('T\<Rightarrow>'T\<Rightarrow>bool))) \<bullet>
           (meta_eq_to_obj_eq \<cdot> TYPE('T) \<cdot> A \<cdot> B \<bullet> prfT \<bullet> prf1)) \<bullet>
         (meta_eq_to_obj_eq \<cdot> TYPE('T) \<cdot> C \<cdot> D \<bullet> prfT \<bullet> prf2)) \<bullet>
       (meta_eq_to_obj_eq \<cdot> TYPE('T) \<cdot> A \<cdot> C \<bullet> prfT \<bullet> prf3))\<close>,
@@ -87,9 +87,9 @@
         prfT \<bullet> arity_type_bool \<bullet>
         (cong \<cdot> TYPE('T) \<cdot> TYPE('T\<Rightarrow>bool) \<cdot>
           ((=) :: 'T\<Rightarrow>'T\<Rightarrow>bool) \<cdot> ((=) :: 'T\<Rightarrow>'T\<Rightarrow>bool) \<cdot> A \<cdot> B \<bullet>
-          prfT \<bullet> (Pure.OfClass type_class \<cdot> TYPE('T\<Rightarrow>bool)) \<bullet>
+          prfT \<bullet> (Pure.PClass type_class \<cdot> TYPE('T\<Rightarrow>bool)) \<bullet>
           (HOL.refl \<cdot> TYPE('T\<Rightarrow>'T\<Rightarrow>bool) \<cdot> ((=) :: 'T\<Rightarrow>'T\<Rightarrow>bool) \<bullet>
-             (Pure.OfClass type_class \<cdot> TYPE('T\<Rightarrow>'T\<Rightarrow>bool))) \<bullet>
+             (Pure.PClass type_class \<cdot> TYPE('T\<Rightarrow>'T\<Rightarrow>bool))) \<bullet>
           (meta_eq_to_obj_eq \<cdot> TYPE('T) \<cdot> A \<cdot> B \<bullet> prfT \<bullet> prf1)) \<bullet>
         (meta_eq_to_obj_eq \<cdot> TYPE('T) \<cdot> C \<cdot> D \<bullet> prfT \<bullet> prf2)) \<bullet>
       (meta_eq_to_obj_eq \<cdot> TYPE('T) \<cdot> B \<cdot> D \<bullet> prfT \<bullet> prf3))\<close>,
@@ -155,7 +155,7 @@
         ((\<and>) :: bool\<Rightarrow>bool\<Rightarrow>bool) \<cdot> ((\<and>) :: bool\<Rightarrow>bool\<Rightarrow>bool) \<cdot> A \<cdot> A \<bullet>
           prfb \<bullet> prfbb \<bullet>
           (HOL.refl \<cdot> TYPE(bool\<Rightarrow>bool\<Rightarrow>bool) \<cdot> ((\<and>) :: bool\<Rightarrow>bool\<Rightarrow>bool) \<bullet>
-             (Pure.OfClass type_class \<cdot> TYPE(bool\<Rightarrow>bool\<Rightarrow>bool))) \<bullet>
+             (Pure.PClass type_class \<cdot> TYPE(bool\<Rightarrow>bool\<Rightarrow>bool))) \<bullet>
           (HOL.refl \<cdot> TYPE(bool) \<cdot> A \<bullet> prfb)))\<close>,
 
    (* \<or> *)
@@ -181,7 +181,7 @@
         ((\<or>) :: bool\<Rightarrow>bool\<Rightarrow>bool) \<cdot> ((\<or>) :: bool\<Rightarrow>bool\<Rightarrow>bool) \<cdot> A \<cdot> A \<bullet>
           prfb \<bullet> prfbb \<bullet>
           (HOL.refl \<cdot> TYPE(bool\<Rightarrow>bool\<Rightarrow>bool) \<cdot> ((\<or>) :: bool\<Rightarrow>bool\<Rightarrow>bool) \<bullet>
-             (Pure.OfClass type_class \<cdot> TYPE(bool\<Rightarrow>bool\<Rightarrow>bool))) \<bullet>
+             (Pure.PClass type_class \<cdot> TYPE(bool\<Rightarrow>bool\<Rightarrow>bool))) \<bullet>
           (HOL.refl \<cdot> TYPE(bool) \<cdot> A \<bullet> prfb)))\<close>,
 
    (* \<longrightarrow> *)
@@ -205,7 +205,7 @@
         ((\<longrightarrow>) :: bool\<Rightarrow>bool\<Rightarrow>bool) \<cdot> ((\<longrightarrow>) :: bool\<Rightarrow>bool\<Rightarrow>bool) \<cdot> A \<cdot> A \<bullet>
           prfb \<bullet> prfbb \<bullet>
           (HOL.refl \<cdot> TYPE(bool\<Rightarrow>bool\<Rightarrow>bool) \<cdot> ((\<longrightarrow>) :: bool\<Rightarrow>bool\<Rightarrow>bool) \<bullet>
-             (Pure.OfClass type_class \<cdot> TYPE(bool\<Rightarrow>bool\<Rightarrow>bool))) \<bullet>
+             (Pure.PClass type_class \<cdot> TYPE(bool\<Rightarrow>bool\<Rightarrow>bool))) \<bullet>
           (HOL.refl \<cdot> TYPE(bool) \<cdot> A \<bullet> prfb)))\<close>,
 
    (* \<not> *)
@@ -257,7 +257,7 @@
         ((=) :: bool\<Rightarrow>bool\<Rightarrow>bool) \<cdot> ((=) :: bool\<Rightarrow>bool\<Rightarrow>bool) \<cdot> A \<cdot> A \<bullet>
           prfb \<bullet> prfbb \<bullet>
           (HOL.refl \<cdot> TYPE(bool\<Rightarrow>bool\<Rightarrow>bool) \<cdot> ((=) :: bool\<Rightarrow>bool\<Rightarrow>bool) \<bullet>
-             (Pure.OfClass type_class \<cdot> TYPE(bool\<Rightarrow>bool\<Rightarrow>bool))) \<bullet>
+             (Pure.PClass type_class \<cdot> TYPE(bool\<Rightarrow>bool\<Rightarrow>bool))) \<bullet>
           (HOL.refl \<cdot> TYPE(bool) \<cdot> A \<bullet> prfb)))\<close>,
 
    (** transitivity, reflexivity, and symmetry **)
diff -r 5ef7f374e0f8 -r 3875815f5967 src/Pure/ML/ml_pp.ML
--- a/src/Pure/ML/ml_pp.ML	Tue Apr 21 22:04:15 2020 +0200
+++ b/src/Pure/ML/ml_pp.ML	Tue Apr 21 22:19:59 2020 +0200
@@ -78,7 +78,7 @@
     | MinProof => Pretty.str "MinProof"
     | PBound a => prt_app "PBound" (Pretty.from_polyml (ML_system_pretty (a, dp - 1)))
     | PAxm a => prt_app "PAxm" (Pretty.from_polyml (ML_system_pretty (a, dp - 1)))
-    | OfClass a => prt_app "OfClass" (Pretty.from_polyml (ML_system_pretty (a, dp - 1)))
+    | PClass a => prt_app "PClass" (Pretty.from_polyml (ML_system_pretty (a, dp - 1)))
     | Oracle a => prt_app "Oracle" (Pretty.from_polyml (ML_system_pretty (a, dp - 1)))
     | PThm a => prt_app "PThm" (Pretty.from_polyml (ML_system_pretty (a, dp - 1))))
 
diff -r 5ef7f374e0f8 -r 3875815f5967 src/Pure/Proof/proof_checker.ML
--- a/src/Pure/Proof/proof_checker.ML	Tue Apr 21 22:04:15 2020 +0200
+++ b/src/Pure/Proof/proof_checker.ML	Tue Apr 21 22:19:59 2020 +0200
@@ -137,11 +137,11 @@
 
           | thm_of _ _ (Hyp t) = Thm.assume (Thm.global_cterm_of thy t)
 
-          | thm_of _ _ (OfClass (T, c)) =
+          | thm_of _ _ (PClass (T, c)) =
               if Sign.of_sort thy (T, [c])
               then Thm.of_class (Thm.global_ctyp_of thy T, c)
               else
-                error ("thm_of_proof: bad OfClass proof " ^
+                error ("thm_of_proof: bad PClass proof " ^
                   Syntax.string_of_term_global thy (Logic.mk_of_class (T, c)))
 
           | thm_of _ _ _ = error "thm_of_proof: partial proof term";
diff -r 5ef7f374e0f8 -r 3875815f5967 src/Pure/Proof/proof_rewrite_rules.ML
--- a/src/Pure/Proof/proof_rewrite_rules.ML	Tue Apr 21 22:04:15 2020 +0200
+++ b/src/Pure/Proof/proof_rewrite_rules.ML	Tue Apr 21 22:19:59 2020 +0200
@@ -344,7 +344,7 @@
   end;
 
 
-(**** expand OfClass proofs ****)
+(**** expand PClass proofs ****)
 
 fun expand_of_sort_proof thy hyps (T, S) =
   let
@@ -367,13 +367,13 @@
   in
     map2 reconstruct (Logic.mk_of_sort (T, S))
       (Proofterm.of_sort_proof (Sign.classes_of thy) (Thm.classrel_proof thy) (Thm.arity_proof thy)
-        (OfClass o apfst Type.strip_sorts) (subst T, S))
+        (PClass o apfst Type.strip_sorts) (subst T, S))
   end;
 
 fun expand_of_class_proof thy hyps (T, c) =
   hd (expand_of_sort_proof thy hyps (T, [c]));
 
-fun expand_of_class thy (_: typ list) hyps (OfClass (T, c)) =
+fun expand_of_class thy (_: typ list) hyps (PClass (T, c)) =
       SOME (expand_of_class_proof thy hyps (T, c), Proofterm.no_skel)
   | expand_of_class _ _ _ _ = NONE;
 
diff -r 5ef7f374e0f8 -r 3875815f5967 src/Pure/Proof/proof_syntax.ML
--- a/src/Pure/Proof/proof_syntax.ML	Tue Apr 21 22:04:15 2020 +0200
+++ b/src/Pure/Proof/proof_syntax.ML	Tue Apr 21 22:19:59 2020 +0200
@@ -100,16 +100,16 @@
 fun AppT T prf =
   Const ("Pure.Appt", proofT --> Term.itselfT T --> proofT) $ prf $ Logic.mk_type T;
 
-fun OfClasst (T, c) =
+fun PClasst (T, c) =
   let val U = Term.itselfT T --> propT
-  in Const ("Pure.OfClass", U --> proofT) $ Const (Logic.const_of_class c, U) end;
+  in Const ("Pure.PClass", U --> proofT) $ Const (Logic.const_of_class c, U) end;
 
 fun term_of _ (PThm ({serial = i, name, types = Ts, ...}, _)) =
       fold AppT (these Ts)
         (Const (Long_Name.append "thm" (if name = "" then string_of_int i else name), proofT))
   | term_of _ (PAxm (name, _, Ts)) =
       fold AppT (these Ts) (Const (Long_Name.append "axm" name, proofT))
-  | term_of _ (OfClass (T, c)) = AppT T (OfClasst (T, c))
+  | term_of _ (PClass (T, c)) = AppT T (PClasst (T, c))
   | term_of _ (PBound i) = Bound i
   | term_of Ts (Abst (s, opT, prf)) =
       let val T = the_default dummyT opT in
@@ -166,11 +166,11 @@
                    | NONE => error ("Unknown theorem " ^ quote name))
                  end
              | _ => error ("Illegal proof constant name: " ^ quote s))
-      | prf_of Ts (Const ("Pure.OfClass", _) $ Const (c_class, _)) =
+      | prf_of Ts (Const ("Pure.PClass", _) $ Const (c_class, _)) =
           (case try Logic.class_of_const c_class of
             SOME c =>
               Proofterm.change_types (if ty then SOME Ts else NONE)
-                (OfClass (TVar ((Name.aT, 0), []), c))
+                (PClass (TVar ((Name.aT, 0), []), c))
           | NONE => error ("Bad class constant: " ^ quote c_class))
       | prf_of Ts (Const ("Pure.Hyp", _) $ prop) = Hyp prop
       | prf_of Ts (v as Var ((_, Type ("Pure.proof", _)))) = Hyp v
diff -r 5ef7f374e0f8 -r 3875815f5967 src/Pure/proofterm.ML
--- a/src/Pure/proofterm.ML	Tue Apr 21 22:04:15 2020 +0200
+++ b/src/Pure/proofterm.ML	Tue Apr 21 22:19:59 2020 +0200
@@ -22,7 +22,7 @@
    | %% of proof * proof
    | Hyp of term
    | PAxm of string * term * typ list option
-   | OfClass of typ * class
+   | PClass of typ * class
    | Oracle of string * term * typ list option
    | PThm of thm_header * thm_body
   and proof_body = PBody of
@@ -214,7 +214,7 @@
  | op %% of proof * proof
  | Hyp of term
  | PAxm of string * term * typ list option
- | OfClass of typ * class
+ | PClass of typ * class
  | Oracle of string * term * typ list option
  | PThm of thm_header * thm_body
 and proof_body = PBody of
@@ -368,7 +368,7 @@
   fn a %% b => ([], pair (proof consts) (proof consts) (a, b)),
   fn Hyp a => ([], term consts a),
   fn PAxm (a, b, c) => ([a], pair (term consts) (option (list typ)) (b, c)),
-  fn OfClass (a, b) => ([b], typ a),
+  fn PClass (a, b) => ([b], typ a),
   fn Oracle (a, b, c) => ([a], pair (term consts) (option (list typ)) (b, c)),
   fn PThm ({serial, pos, theory_name, name, prop, types}, Thm_Body {open_proof, body, ...}) =>
     ([int_atom serial, theory_name, name],
@@ -399,7 +399,7 @@
   fn a %% b => ([], pair (standard_proof consts) (standard_proof consts) (a, b)),
   fn Hyp a => ([], standard_term consts a),
   fn PAxm (name, _, SOME Ts) => ([name], list typ Ts),
-  fn OfClass (T, c) => ([c], typ T),
+  fn PClass (T, c) => ([c], typ T),
   fn Oracle (name, prop, SOME Ts) => ([name], pair (standard_term consts) (list typ) (prop, Ts)),
   fn PThm ({serial, theory_name, name, types = SOME Ts, ...}, _) =>
     ([int_atom serial, theory_name, name], list typ Ts)];
@@ -429,7 +429,7 @@
   fn ([], a) => op %% (pair (proof consts) (proof consts) a),
   fn ([], a) => Hyp (term consts a),
   fn ([a], b) => let val (c, d) = pair (term consts) (option (list typ)) b in PAxm (a, c, d) end,
-  fn ([b], a) => OfClass (typ a, b),
+  fn ([b], a) => PClass (typ a, b),
   fn ([a], b) => let val (c, d) = pair (term consts) (option (list typ)) b in Oracle (a, c, d) end,
   fn ([a, b, c], d) =>
     let
@@ -516,14 +516,14 @@
           (proof prf1 %% Same.commit proof prf2
             handle Same.SAME => prf1 %% proof prf2)
       | proof (PAxm (a, prop, SOME Ts)) = PAxm (a, prop, SOME (typs Ts))
-      | proof (OfClass T_c) = ofclass T_c
+      | proof (PClass T_c) = ofclass T_c
       | proof (Oracle (a, prop, SOME Ts)) = Oracle (a, prop, SOME (typs Ts))
       | proof (PThm ({serial, pos, theory_name, name, prop, types = SOME Ts}, thm_body)) =
           PThm (thm_header serial pos theory_name name prop (SOME (typs Ts)), thm_body)
       | proof _ = raise Same.SAME;
   in proof end;
 
-fun map_proof_terms_same term typ = map_proof_same term typ (fn (T, c) => OfClass (typ T, c));
+fun map_proof_terms_same term typ = map_proof_same term typ (fn (T, c) => PClass (typ T, c));
 fun map_proof_types_same typ = map_proof_terms_same (Term_Subst.map_types_same typ) typ;
 
 fun same eq f x =
@@ -550,7 +550,7 @@
   | fold_proof_terms_types f g (prf1 %% prf2) =
       fold_proof_terms_types f g prf1 #> fold_proof_terms_types f g prf2
   | fold_proof_terms_types _ g (PAxm (_, _, SOME Ts)) = fold g Ts
-  | fold_proof_terms_types _ g (OfClass (T, _)) = g T
+  | fold_proof_terms_types _ g (PClass (T, _)) = g T
   | fold_proof_terms_types _ g (Oracle (_, _, SOME Ts)) = fold g Ts
   | fold_proof_terms_types _ g (PThm ({types = SOME Ts, ...}, _)) = fold g Ts
   | fold_proof_terms_types _ _ _ = I;
@@ -564,7 +564,7 @@
   | size_of_proof _ = 1;
 
 fun change_types types (PAxm (name, prop, _)) = PAxm (name, prop, types)
-  | change_types (SOME [T]) (OfClass (_, c)) = OfClass (T, c)
+  | change_types (SOME [T]) (PClass (_, c)) = PClass (T, c)
   | change_types types (Oracle (name, prop, _)) = Oracle (name, prop, types)
   | change_types types (PThm ({serial, pos, theory_name, name, prop, types = _}, thm_body)) =
       PThm (thm_header serial pos theory_name name prop types, thm_body)
@@ -710,8 +710,8 @@
             handle Same.SAME => prf1 %% norm prf2)
       | norm (PAxm (s, prop, Ts)) =
           PAxm (s, prop, Same.map_option (htypeTs Envir.norm_types_same) Ts)
-      | norm (OfClass (T, c)) =
-          OfClass (htypeT Envir.norm_type_same T, c)
+      | norm (PClass (T, c)) =
+          PClass (htypeT Envir.norm_type_same T, c)
       | norm (Oracle (s, prop, Ts)) =
           Oracle (s, prop, Same.map_option (htypeTs Envir.norm_types_same) Ts)
       | norm (PThm ({serial = i, pos = p, theory_name, name = a, prop = t, types = Ts}, thm_body)) =
@@ -990,8 +990,8 @@
           handle Same.SAME => prf1 %% lift' Us Ts prf2)
       | lift' _ _ (PAxm (s, prop, Ts)) =
           PAxm (s, prop, (Same.map_option o Same.map) (Logic.incr_tvar_same inc) Ts)
-      | lift' _ _ (OfClass (T, c)) =
-          OfClass (Logic.incr_tvar_same inc T, c)
+      | lift' _ _ (PClass (T, c)) =
+          PClass (Logic.incr_tvar_same inc T, c)
       | lift' _ _ (Oracle (s, prop, Ts)) =
           Oracle (s, prop, (Same.map_option o Same.map) (Logic.incr_tvar_same inc) Ts)
       | lift' _ _ (PThm ({serial = i, pos = p, theory_name, name = s, prop, types = Ts}, thm_body)) =
@@ -1162,7 +1162,7 @@
     val args = prop_args prop;
     val ({outer_constraints, ...}, prop1) = Logic.unconstrainT [] prop;
     val head = mk (name, prop1, NONE);
-  in proof_combP (proof_combt' (head, args), map OfClass outer_constraints) end;
+  in proof_combP (proof_combt' (head, args), map PClass outer_constraints) end;
 
 val axm_proof = const_proof PAxm;
 val oracle_proof = const_proof Oracle;
@@ -1198,7 +1198,7 @@
              orelse exists #1 prfs then [i] else [], false, map (pair false) ts, prf)
       | shrink' _ _ ts _ (Hyp t) = ([], false, map (pair false) ts, Hyp t)
       | shrink' _ _ ts _ (prf as MinProof) = ([], false, map (pair false) ts, prf)
-      | shrink' _ _ ts _ (prf as OfClass _) = ([], false, map (pair false) ts, prf)
+      | shrink' _ _ ts _ (prf as PClass _) = ([], false, map (pair false) ts, prf)
       | shrink' _ _ ts prfs prf =
           let
             val prop =
@@ -1378,7 +1378,7 @@
       | mtch Ts i j inst (PAxm (s1, _, opTs), PAxm (s2, _, opUs)) =
           if s1 = s2 then optmatch matchTs inst (opTs, opUs)
           else raise PMatch
-      | mtch Ts i j inst (OfClass (T1, c1), OfClass (T2, c2)) =
+      | mtch Ts i j inst (PClass (T1, c1), PClass (T2, c2)) =
           if c1 = c2 then matchT inst (T1, T2)
           else raise PMatch
       | mtch Ts i j inst
@@ -1427,7 +1427,7 @@
             NONE => raise Same.SAME
           | SOME prf' => incr_pboundvars plev tlev prf')
       | subst _ _ (PAxm (id, prop, Ts)) = PAxm (id, prop, Same.map_option substTs Ts)
-      | subst _ _ (OfClass (T, c)) = OfClass (substT T, c)
+      | subst _ _ (PClass (T, c)) = PClass (substT T, c)
       | subst _ _ (Oracle (id, prop, Ts)) = Oracle (id, prop, Same.map_option substTs Ts)
       | subst _ _ (PThm ({serial = i, pos = p, theory_name, name = id, prop, types}, thm_body)) =
           PThm (thm_header i p theory_name id prop (Same.map_option substTs types), thm_body)
@@ -1453,7 +1453,7 @@
         (_, Hyp (Var _)) => true
       | (Hyp (Var _), _) => true
       | (PAxm (a, _, _), PAxm (b, _, _)) => a = b andalso matchrands prf1 prf2
-      | (OfClass (_, c), OfClass (_, d)) => c = d andalso matchrands prf1 prf2
+      | (PClass (_, c), PClass (_, d)) => c = d andalso matchrands prf1 prf2
       | (PThm ({name = a, prop = propa, ...}, _), PThm ({name = b, prop = propb, ...}, _)) =>
           a = b andalso propa = propb andalso matchrands prf1 prf2
       | (PBound i, PBound j) => i = j andalso matchrands prf1 prf2
@@ -1607,7 +1607,7 @@
 
 fun guess_name (PThm ({name, ...}, _)) = name
   | guess_name (prf %% Hyp _) = guess_name prf
-  | guess_name (prf %% OfClass _) = guess_name prf
+  | guess_name (prf %% PClass _) = guess_name prf
   | guess_name (prf % NONE) = guess_name prf
   | guess_name (prf % SOME (Var _)) = guess_name prf
   | guess_name _ = "";
@@ -1801,7 +1801,7 @@
           mk_cnstrts_atom env vTs prop opTs prf
       | mk_cnstrts env _ _ vTs (prf as PAxm (_, prop, opTs)) =
           mk_cnstrts_atom env vTs prop opTs prf
-      | mk_cnstrts env _ _ vTs (prf as OfClass (T, c)) =
+      | mk_cnstrts env _ _ vTs (prf as PClass (T, c)) =
           mk_cnstrts_atom env vTs (Logic.mk_of_class (T, c)) NONE prf
       | mk_cnstrts env _ _ vTs (prf as Oracle (_, prop, opTs)) =
           mk_cnstrts_atom env vTs prop opTs prf
@@ -1899,7 +1899,7 @@
   | prop_of0 _ (Hyp t) = t
   | prop_of0 _ (PThm ({prop, types = SOME Ts, ...}, _)) = prop_of_atom prop Ts
   | prop_of0 _ (PAxm (_, prop, SOME Ts)) = prop_of_atom prop Ts
-  | prop_of0 _ (OfClass (T, c)) = Logic.mk_of_class (T, c)
+  | prop_of0 _ (PClass (T, c)) = Logic.mk_of_class (T, c)
   | prop_of0 _ (Oracle (_, prop, SOME Ts)) = prop_of_atom prop Ts
   | prop_of0 _ _ = error "prop_of: partial proof object";
 
@@ -2233,7 +2233,7 @@
         proof_combt' (head, (map o Option.map o Term.map_types) (#map_atyps ucontext) args)
       else
         proof_combP (proof_combt' (head, args),
-          map OfClass (#outer_constraints ucontext) @ map Hyp hyps);
+          map PClass (#outer_constraints ucontext) @ map Hyp hyps);
   in (thm, proof) end;
 
 in
diff -r 5ef7f374e0f8 -r 3875815f5967 src/Pure/pure_thy.ML
--- a/src/Pure/pure_thy.ML	Tue Apr 21 22:04:15 2020 +0200
+++ b/src/Pure/pure_thy.ML	Tue Apr 21 22:19:59 2020 +0200
@@ -223,7 +223,7 @@
     (qualify (Binding.make ("AbsP", \<^here>)), typ "prop \<Rightarrow> (Pure.proof \<Rightarrow> Pure.proof) \<Rightarrow> Pure.proof", NoSyn),
     (qualify (Binding.make ("Hyp", \<^here>)), typ "prop \<Rightarrow> Pure.proof", NoSyn),
     (qualify (Binding.make ("Oracle", \<^here>)), typ "prop \<Rightarrow> Pure.proof", NoSyn),
-    (qualify (Binding.make ("OfClass", \<^here>)), typ "('a itself \<Rightarrow> prop) \<Rightarrow> Pure.proof", NoSyn),
+    (qualify (Binding.make ("PClass", \<^here>)), typ "('a itself \<Rightarrow> prop) \<Rightarrow> Pure.proof", NoSyn),
     (qualify (Binding.make ("MinProof", \<^here>)), typ "Pure.proof", NoSyn)]
   #> add_deps_const "Pure.eq"
   #> add_deps_const "Pure.imp"
diff -r 5ef7f374e0f8 -r 3875815f5967 src/Pure/pure_thy.scala
--- a/src/Pure/pure_thy.scala	Tue Apr 21 22:04:15 2020 +0200
+++ b/src/Pure/pure_thy.scala	Tue Apr 21 22:19:59 2020 +0200
@@ -32,6 +32,6 @@
   val ABSP: String = "Pure.AbsP"
   val HYP: String = "Pure.Hyp"
   val ORACLE: String = "Pure.Oracle"
-  val OFCLASS: String = "Pure.OfClass"
+  val OFCLASS: String = "Pure.PClass"
   val MINPROOF: String = "Pure.MinProof"
 }
diff -r 5ef7f374e0f8 -r 3875815f5967 src/Pure/term.scala
--- a/src/Pure/term.scala	Tue Apr 21 22:04:15 2020 +0200
+++ b/src/Pure/term.scala	Tue Apr 21 22:19:59 2020 +0200
@@ -99,7 +99,7 @@
   case class AppP(fun: Proof, arg: Proof) extends Proof
   case class Hyp(hyp: Term) extends Proof
   case class PAxm(name: String, types: List[Typ]) extends Proof
-  case class OfClass(typ: Typ, cls: Class) extends Proof
+  case class PClass(typ: Typ, cls: Class) extends Proof
   case class Oracle(name: String, prop: Term, types: List[Typ]) extends Proof
   case class PThm(serial: Long, theory_name: String, name: String, types: List[Typ]) extends Proof
 
@@ -205,7 +205,7 @@
               case AppP(fun, arg) => store(AppP(cache_proof(fun), cache_proof(arg)))
               case Hyp(hyp) => store(Hyp(cache_term(hyp)))
               case PAxm(name, types) => store(PAxm(cache_string(name), cache_typs(types)))
-              case OfClass(typ, cls) => store(OfClass(cache_typ(typ), cache_string(cls)))
+              case PClass(typ, cls) => store(PClass(cache_typ(typ), cache_string(cls)))
               case Oracle(name, prop, types) =>
                 store(Oracle(cache_string(name), cache_term(prop), cache_typs(types)))
               case PThm(serial, theory_name, name, types) =>
diff -r 5ef7f374e0f8 -r 3875815f5967 src/Pure/term_xml.scala
--- a/src/Pure/term_xml.scala	Tue Apr 21 22:04:15 2020 +0200
+++ b/src/Pure/term_xml.scala	Tue Apr 21 22:19:59 2020 +0200
@@ -95,7 +95,7 @@
           { case (Nil, a) => val (b, c) = pair(proof, proof)(a); AppP(b, c) },
           { case (Nil, a) => Hyp(term(a)) },
           { case (List(a), b) => PAxm(a, list(typ)(b)) },
-          { case (List(a), b) => OfClass(typ(b), a) },
+          { case (List(a), b) => PClass(typ(b), a) },
           { case (List(a), b) => val (c, d) = pair(term, list(typ))(b); Oracle(a, c, d) },
           { case (List(a, b, c), d) => PThm(long_atom(a), b, c, list(typ)(d)) }))
       proof
diff -r 5ef7f374e0f8 -r 3875815f5967 src/Pure/thm.ML
--- a/src/Pure/thm.ML	Tue Apr 21 22:04:15 2020 +0200
+++ b/src/Pure/thm.ML	Tue Apr 21 22:19:59 2020 +0200
@@ -1719,7 +1719,7 @@
     val Cterm {t = prop, maxidx, sorts, ...} = global_cterm_of thy (Logic.mk_of_class (T, c));
   in
     if Sign.of_sort thy (T, [c]) then
-      Thm (deriv_rule0 (fn () => Proofterm.OfClass (T, c)),
+      Thm (deriv_rule0 (fn () => Proofterm.PClass (T, c)),
        {cert = cert,
         tags = [],
         maxidx = maxidx,