tuned signature;

--- a/src/Pure/proofterm.ML	Sun Dec 31 19:24:37 2023 +0100
+++ b/src/Pure/proofterm.ML	Sun Dec 31 21:40:14 2023 +0100
@@ -147,7 +147,7 @@
   val could_unify: proof * proof -> bool
   type sorts_proof = (class * class -> proof) * (string * class list list * class -> proof)
   val of_sort_proof: Sorts.algebra -> sorts_proof -> (typ * class -> proof) -> typ * sort -> proof list
-  val axm_proof: string -> term -> proof
+  val axiom_proof: string -> term -> proof
   val oracle_proof: string -> term -> proof
   val shrink_proof: proof -> proof
 
@@ -1201,7 +1201,7 @@
     val head = mk (name, prop1, NONE);
   in proof_combP (proof_combt' (head, args), map PClass outer_constraints) end;
 
-val axm_proof = const_proof PAxm;
+val axiom_proof = const_proof PAxm;
 val oracle_proof = const_proof Oracle;
 
 val shrink_proof =

--- a/src/Pure/thm.ML	Sun Dec 31 19:24:37 2023 +0100
+++ b/src/Pure/thm.ML	Sun Dec 31 21:40:14 2023 +0100
@@ -870,7 +870,7 @@
     SOME prop =>
       let
         fun zproof () = ZTerm.axiom_proof thy name prop;
-        fun proof () = Proofterm.axm_proof name prop;
+        fun proof () = Proofterm.axiom_proof name prop;
         val cert = Context.Certificate thy;
         val maxidx = maxidx_of_term prop;
         val shyps = Sorts.insert_term prop [];