# HG changeset patch
# User wenzelm
# Date 1453299738 -3600
# Node ID c56c2d50dd6d95f73f768ed00df8c6ad027c0364
# Parent  8addfff5965a241cddaa65d2f9b8d195fd64edf1
tuned;

diff -r 8addfff5965a -r c56c2d50dd6d src/Pure/General/antiquote.ML
--- a/src/Pure/General/antiquote.ML	Wed Jan 20 15:17:03 2016 +0100
+++ b/src/Pure/General/antiquote.ML	Wed Jan 20 15:22:18 2016 +0100
@@ -79,7 +79,7 @@
 val scan_txt =
   Scan.repeats1
    (Scan.many1 (fn (s, _) =>
-      not (Symbol.is_control s) andalso s <> "\\<open>" andalso s <> "@" andalso Symbol.not_eof s) ||
+      not (Symbol.is_control s) andalso s <> Symbol.open_ andalso s <> "@" andalso Symbol.not_eof s) ||
     $$$ "@" --| Scan.ahead (~$$ "{"));
 
 val scan_antiq_body =