src/Pure/thm.ML
changeset 79410 719563e4816a
parent 79409 e1895596e1b9
child 79413 9495bd0112d7
--- 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 [];