# HG changeset patch
# User wenzelm
# Date 1621546434 -7200
# Node ID 736c1b239b9d1eb31e1e491e59c4a1b0e2c63f00
# Parent  cb933ba9ecfe484a58755ce81823b459f74cb9af
clarified, e.g. type variables;

diff -r cb933ba9ecfe -r 736c1b239b9d 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 ""