# HG changeset patch
# User wenzelm
# Date 1390070142 -3600
# Node ID 87797f8f3152c6cd2eedf18b19ef7a9a3962dcae
# Parent  68afbb5ce4ffd675641bcd2d971d9e626f665a6e
proper \<newline>;

diff -r 68afbb5ce4ff -r 87797f8f3152 src/HOL/ex/Cartouche_Examples.thy
--- a/src/HOL/ex/Cartouche_Examples.thy	Sat Jan 18 19:31:32 2014 +0100
+++ b/src/HOL/ex/Cartouche_Examples.thy	Sat Jan 18 19:35:42 2014 +0100
@@ -31,7 +31,7 @@
       let
         val c =
           if Symbol.is_ascii s then ord s
-          else if s = "" then 10
+          else if s = "\<newline>" then 10
           else error ("String literal contains illegal symbol: " ^ quote s ^ Position.here pos);
       in Syntax.const @{const_syntax Char} $ mk_nib (c div 16) $ mk_nib (c mod 16) end;