clarified, e.g. type variables;
authorwenzelm
Thu, 20 May 2021 23:33:54 +0200
changeset 74014 736c1b239b9d
parent 74013 cb933ba9ecfe
child 74015 74078d50d77b
clarified, e.g. type variables;
src/Pure/Thy/document_antiquotations.ML
--- 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 ""