# HG changeset patch # User wenzelm # Date 1701716583 -3600 # Node ID f9390f5399ae3a4d93df17962d8b61ab6ccce9e4 # Parent 6a84d18fa548da2e4db2630719cd29899e97ed11 tuned; diff -r 6a84d18fa548 -r f9390f5399ae src/Pure/proofterm.ML --- a/src/Pure/proofterm.ML Mon Dec 04 19:24:39 2023 +0100 +++ b/src/Pure/proofterm.ML Mon Dec 04 20:03:03 2023 +0100 @@ -1285,13 +1285,14 @@ (** axioms for equality **) +local val thy = Sign.local_path (Context.the_global_context ()) in + val [reflexive_axm, symmetric_axm, transitive_axm, equal_intr_axm, equal_elim_axm, abstract_rule_axm, combination_axm] = - 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); + map (fn (b, t) => PAxm (Sign.full_name thy b, Logic.varify_global t, NONE)) + Theory.equality_axioms; + +end; val reflexive_proof = reflexive_axm % NONE;