author | wenzelm |
Thu, 20 May 2021 23:33:54 +0200 | |
changeset 73758 | 736c1b239b9d |
parent 73757 | cb933ba9ecfe |
child 73759 | 74078d50d77b |
--- a/src/Pure/Thy/document_antiquotations.ML Thu May 20 22:02:19 2021 +0200 +++ b/src/Pure/Thy/document_antiquotations.ML Thu May 20 23:33:54 2021 +0200 @@ -146,7 +146,7 @@ local -val strip_symbols = [Symbol.open_, Symbol.close, "\"", "`"]; +val strip_symbols = [Symbol.open_, Symbol.close, "'", "\"", "`"]; fun strip_symbol sym = if member (op =) strip_symbols sym then ""