src/Pure/Syntax/syntax_ext.ML
changeset 71545 b0b16088ccf2
parent 69584 a91e32843310
child 77999 ec850750db87
--- a/src/Pure/Syntax/syntax_ext.ML	Thu Mar 12 23:05:11 2020 +0100
+++ b/src/Pure/Syntax/syntax_ext.ML	Fri Mar 13 16:04:27 2020 +0100
@@ -243,7 +243,7 @@
 val read_block_indent =
   Bg o block_indent o #1 o Library.read_int o map Symbol_Pos.symbol;
 
-val is_meta = member (op =) ["(", ")", "/", "_", "\<index>", Symbol.open_, Symbol.close];
+val is_meta = member (op =) ["'", "(", ")", "/", "_", "\<index>", Symbol.open_, Symbol.close];
 
 val scan_delim =
   scan_one Symbol.is_control ::: Symbol_Pos.scan_cartouche "Mixfix error: " ||