# HG changeset patch
# User wenzelm
# Date 1165869665 -3600
# Node ID 8be8da44ee56072e168421a74730a3e304a51cc1
# Parent  3f9324ff06e3ee2fcd4681acd1b8b4fec95f1b82
specials: include single quote;

diff -r 3f9324ff06e3 -r 8be8da44ee56 src/HOL/Tools/string_syntax.ML
--- a/src/HOL/Tools/string_syntax.ML	Mon Dec 11 21:41:03 2006 +0100
+++ b/src/HOL/Tools/string_syntax.ML	Mon Dec 11 21:41:05 2006 +0100
@@ -32,7 +32,7 @@
     Syntax.Appl [Syntax.Constant "Char", mk_nib (ord s div 16), mk_nib (ord s mod 16)]
   else error ("Non-ASCII symbol: " ^ quote s);
 
-val specials = explode "\\\"`";
+val specials = explode "\\\"`'";
 
 fun dest_chr c1 c2 =
   let val c = chr (dest_nib c1 * 16 + dest_nib c2) in