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 [];