# HG changeset patch
# User wenzelm
# Date 1704224062 -3600
# Node ID 740ec03b0b7129f613f72ca6c866a72223ca70f9
# Parent  6cacfbce33ba8a5e781adf485d17fd8a8c9fa618
tuned names;

diff -r 6cacfbce33ba -r 740ec03b0b71 src/Pure/proofterm.ML
--- a/src/Pure/proofterm.ML	Tue Jan 02 20:09:42 2024 +0100
+++ b/src/Pure/proofterm.ML	Tue Jan 02 20:34:22 2024 +0100
@@ -544,7 +544,7 @@
           (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 (PClass T_c) = ofclass T_c
+      | proof (PClass C) = ofclass 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)
@@ -1813,8 +1813,8 @@
           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 PClass (T, c)) =
-          mk_cnstrts_atom env vTs (Logic.mk_of_class (T, c)) NONE prf
+      | mk_cnstrts env _ _ vTs (prf as PClass C) =
+          mk_cnstrts_atom env vTs (Logic.mk_of_class C) NONE prf
       | mk_cnstrts env _ _ vTs (prf as Oracle (_, prop, opTs)) =
           mk_cnstrts_atom env vTs prop opTs prf
       | mk_cnstrts env _ _ vTs (Hyp t) = (t, Hyp t, [], env, vTs)
@@ -1911,7 +1911,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 _ (PClass (T, c)) = Logic.mk_of_class (T, c)
+  | prop_of0 _ (PClass C) = Logic.mk_of_class C
   | prop_of0 _ (Oracle (_, prop, SOME Ts)) = prop_of_atom prop Ts
   | prop_of0 _ _ = error "prop_of: partial proof object";
 
diff -r 6cacfbce33ba -r 740ec03b0b71 src/Pure/zterm.ML
--- a/src/Pure/zterm.ML	Tue Jan 02 20:09:42 2024 +0100
+++ b/src/Pure/zterm.ML	Tue Jan 02 20:34:22 2024 +0100
@@ -545,7 +545,7 @@
 
 fun map_class_proof class =
   let
-    fun proof (ZClassp T_c) = class T_c
+    fun proof (ZClassp C) = class C
       | proof (ZAbst (a, T, p)) = ZAbst (a, T, proof p)
       | proof (ZAbsp (a, t, p)) = ZAbsp (a, t, proof p)
       | proof (ZAppt (p, t)) = ZAppt (proof p, t)