# HG changeset patch
# User wenzelm
# Date 1662405638 -7200
# Node ID 0a6a138346da041c6dff79b5e49289934298c0a9
# Parent  6dc5968b9a860ddc662de53977f2c8a5b4a02b58
unused (see 15758fced053);

diff -r 6dc5968b9a86 -r 0a6a138346da src/Pure/Isar/proof_display.ML
--- a/src/Pure/Isar/proof_display.ML	Mon Sep 05 21:18:40 2022 +0200
+++ b/src/Pure/Isar/proof_display.ML	Mon Sep 05 21:20:38 2022 +0200
@@ -100,9 +100,6 @@
     fun pretty_abbrev (c, (ty, t)) = Pretty.block
       (prt_const (c, ty) @ [Pretty.str " \<equiv>", Pretty.brk 1, prt_term_no_vars t]);
 
-    fun pretty_axm (a, t) =
-      Pretty.block [Pretty.mark_str a, Pretty.str ":", Pretty.brk 1, prt_term_no_vars t];
-
     val tsig = Sign.tsig_of thy;
     val consts = Sign.consts_of thy;
     val {const_space, constants, constraints} = Consts.dest consts;