--- a/src/Pure/proofterm.ML Mon Dec 04 10:53:32 2023 +0100
+++ b/src/Pure/proofterm.ML Mon Dec 04 12:10:39 2023 +0100
@@ -132,7 +132,6 @@
val assumption_proof: term list -> term -> int -> proof -> proof
val bicompose_proof: bool -> term list -> term list -> term option -> term list ->
int -> int -> proof -> proof -> proof
- val equality_axms: (string * term) list
val reflexive_axm: proof
val symmetric_axm: proof
val transitive_axm: proof
@@ -1286,34 +1285,13 @@
(** axioms for equality **)
-val aT = TFree ("'a", []);
-val bT = TFree ("'b", []);
-val x = Free ("x", aT);
-val y = Free ("y", aT);
-val z = Free ("z", aT);
-val A = Free ("A", propT);
-val B = Free ("B", propT);
-val f = Free ("f", aT --> bT);
-val g = Free ("g", aT --> bT);
-
-val equality_axms =
- [("reflexive", Logic.mk_equals (x, x)),
- ("symmetric", Logic.mk_implies (Logic.mk_equals (x, y), Logic.mk_equals (y, x))),
- ("transitive",
- Logic.list_implies ([Logic.mk_equals (x, y), Logic.mk_equals (y, z)], Logic.mk_equals (x, z))),
- ("equal_intr",
- Logic.list_implies ([Logic.mk_implies (A, B), Logic.mk_implies (B, A)], Logic.mk_equals (A, B))),
- ("equal_elim", Logic.list_implies ([Logic.mk_equals (A, B), A], B)),
- ("abstract_rule",
- Logic.mk_implies
- (Logic.all x (Logic.mk_equals (f $ x, g $ x)),
- Logic.mk_equals (lambda x (f $ x), lambda x (g $ x)))),
- ("combination", Logic.list_implies
- ([Logic.mk_equals (f, g), Logic.mk_equals (x, y)], Logic.mk_equals (f $ x, g $ y)))];
-
val [reflexive_axm, symmetric_axm, transitive_axm, equal_intr_axm,
equal_elim_axm, abstract_rule_axm, combination_axm] =
- map (fn (s, t) => PAxm ("Pure." ^ s, Logic.varify_global t, NONE)) equality_axms;
+ Theory.equality_axioms |> map (fn (b, t) =>
+ let
+ val a = Sign.full_name (Sign.local_path (Context.the_global_context ())) b;
+ val A = Logic.varify_global t;
+ in PAxm (a, A, NONE) end);
val reflexive_proof = reflexive_axm % NONE;