changeset 80939 | 3eca969b3c43 |
parent 80875 | 2e33897071b6 |
child 82583 | abd3885a3fcf |
--- a/src/Pure/Tools/find_consts.ML Tue Sep 24 17:35:24 2024 +0200 +++ b/src/Pure/Tools/find_consts.ML Tue Sep 24 17:41:05 2024 +0200 @@ -65,7 +65,7 @@ val markup = Name_Space.markup (Proof_Context.const_space ctxt) c; in Pretty.block - [Pretty.mark markup (Pretty.str c), Pretty.str " ::", Pretty.brk 1, + [Pretty.mark_str (markup, c), Pretty.str " ::", Pretty.brk 1, Pretty.quote (Syntax.pretty_typ ctxt ty')] end;