# HG changeset patch
# User wenzelm
# Date 1701688239 -3600
# Node ID 45b2171e9e034b29870ebdca045818fe455c52f0
# Parent  cf29db6c95e1c0a79670ad5680659d26b82065e9
clarified modules;
more source positions;

diff -r cf29db6c95e1 -r 45b2171e9e03 src/Pure/proofterm.ML
--- 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;
 
diff -r cf29db6c95e1 -r 45b2171e9e03 src/Pure/pure_thy.ML
--- a/src/Pure/pure_thy.ML	Mon Dec 04 10:53:32 2023 +0100
+++ b/src/Pure/pure_thy.ML	Mon Dec 04 12:10:39 2023 +0100
@@ -235,7 +235,6 @@
       \ (CONST Pure.term :: 'a itself \<Rightarrow> prop) (CONST Pure.type :: 'a itself)"),
     (Binding.make ("conjunction_def", \<^here>),
       prop "(A &&& B) \<equiv> (\<And>C::prop. (A \<Longrightarrow> B \<Longrightarrow> C) \<Longrightarrow> C)")] #> snd
-  #> fold (fn (a, prop) =>
-      snd o Thm.add_axiom_global (Binding.make (a, \<^here>), prop)) Proofterm.equality_axms);
+  #> fold (#2 oo Thm.add_axiom_global) Theory.equality_axioms);
 
 end;
diff -r cf29db6c95e1 -r 45b2171e9e03 src/Pure/theory.ML
--- a/src/Pure/theory.ML	Mon Dec 04 10:53:32 2023 +0100
+++ b/src/Pure/theory.ML	Mon Dec 04 12:10:39 2023 +0100
@@ -38,6 +38,7 @@
   val add_def: Defs.context -> bool -> bool -> binding * term -> theory -> theory
   val specify_const: (binding * typ) * mixfix -> theory -> term * theory
   val check_overloading: Proof.context -> bool -> string * typ -> unit
+  val equality_axioms: (binding * term) list
 end
 
 structure Theory: THEORY =
@@ -357,4 +358,39 @@
 
 end;
 
+
+(** axioms for equality **)
+
+local
+
+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);
+
+in
+
+val equality_axioms =
+ [(Binding.make ("reflexive", \<^here>), Logic.mk_equals (x, x)),
+  (Binding.make ("symmetric", \<^here>),
+    Logic.mk_implies (Logic.mk_equals (x, y), Logic.mk_equals (y, x))),
+  (Binding.make ("transitive", \<^here>),
+    Logic.list_implies ([Logic.mk_equals (x, y), Logic.mk_equals (y, z)], Logic.mk_equals (x, z))),
+  (Binding.make ("equal_intr", \<^here>),
+    Logic.list_implies ([Logic.mk_implies (A, B), Logic.mk_implies (B, A)], Logic.mk_equals (A, B))),
+  (Binding.make ("equal_elim", \<^here>), Logic.list_implies ([Logic.mk_equals (A, B), A], B)),
+  (Binding.make ("abstract_rule", \<^here>),
+    Logic.mk_implies
+      (Logic.all x (Logic.mk_equals (f $ x, g $ x)),
+        Logic.mk_equals (lambda x (f $ x), lambda x (g $ x)))),
+  (Binding.make ("combination", \<^here>), Logic.list_implies
+    ([Logic.mk_equals (f, g), Logic.mk_equals (x, y)], Logic.mk_equals (f $ x, g $ y)))];
+
 end;
+
+end;