# 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)