diff -r 317e9ebbc3e1 -r b0b16088ccf2 src/Pure/Syntax/syntax_ext.ML --- 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 =) ["(", ")", "/", "_", "\", Symbol.open_, Symbol.close]; +val is_meta = member (op =) ["'", "(", ")", "/", "_", "\", Symbol.open_, Symbol.close]; val scan_delim = scan_one Symbol.is_control ::: Symbol_Pos.scan_cartouche "Mixfix error: " ||