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