# HG changeset patch
# User wenzelm
# Date 880027250 -3600
# Node ID 901f690e3a58a84a0893ada23eec0677745573c3
# Parent  d5ccc8321e1e341b92779ffab89c09d4a5eab3d4
fixed xstr token encoding;

diff -r d5ccc8321e1e -r 901f690e3a58 src/HOL/ex/String.thy
--- a/src/HOL/ex/String.thy	Thu Nov 20 12:59:20 1997 +0100
+++ b/src/HOL/ex/String.thy	Thu Nov 20 13:00:50 1997 +0100
@@ -1,7 +1,7 @@
 (*  Title:      HOL/String.thy
     ID:         $Id$
 
-Hex chars. Strings.
+Hex chars and strings.
 *)
 
 String = List +
@@ -26,10 +26,6 @@
 ML
 
 local
-  open Syntax;
-
-  val ssquote = enclose "''" "''";
-
 
   (* chars *)
 
@@ -37,7 +33,7 @@
   val ten = ord "A" - 10;
 
   fun mk_nib n =
-    const ("H0" ^ chr (n + (if n <= 9 then zero else ten)));
+    Syntax.const ("H0" ^ chr (n + (if n <= 9 then zero else ten)));
 
   fun dest_nib (Const (c, _)) =
         (case explode c of
@@ -49,42 +45,43 @@
 
 
   fun mk_char c =
-    const "Char" $ mk_nib (ord c div 16) $ mk_nib (ord c mod 16);
+    Syntax.const "Char" $ mk_nib (ord c div 16) $ mk_nib (ord c mod 16);
 
   fun dest_char (Const ("Char", _) $ t1 $ t2) = dest_nibs t1 t2
     | dest_char _ = raise Match;
 
 
-  fun char_tr (*"_Char"*) [Free (c, _)] =
-        if size c = 1 then mk_char c
-        else error ("Bad character: " ^ quote c)
+  fun char_tr (*"_Char"*) [Free (xstr, _)] =
+        (case Syntax.explode_xstr xstr of
+          [c] => mk_char c
+        | _ => error ("Single character expected: " ^ xstr))
     | char_tr (*"_Char"*) ts = raise TERM ("char_tr", ts);
 
   fun char_tr' (*"Char"*) [t1, t2] =
-        const "_Char" $ free (ssquote (dest_nibs t1 t2))
+        Syntax.const "_Char" $ Syntax.free (Syntax.implode_xstr [dest_nibs t1 t2])
     | char_tr' (*"Char"*) _ = raise Match;
 
 
   (* strings *)
 
-  fun mk_string [] = const constrainC $ const "[]" $ const "string"
-    | mk_string (t :: ts) = const "op #" $ t $ mk_string ts;
+  fun mk_string [] = Syntax.const Syntax.constrainC $ Syntax.const "[]" $ Syntax.const "string"
+    | mk_string (t :: ts) = Syntax.const "op #" $ t $ mk_string ts;
 
   fun dest_string (Const ("[]", _)) = []
     | dest_string (Const ("op #", _) $ c $ cs) = dest_char c :: dest_string cs
     | dest_string _ = raise Match;
 
 
-  fun string_tr (*"_String"*) [Free (txt, _)] =
-        mk_string (map mk_char (explode txt))
+  fun string_tr (*"_String"*) [Free (xstr, _)] =
+        mk_string (map mk_char (Syntax.explode_xstr xstr))
     | string_tr (*"_String"*) ts = raise TERM ("string_tr", ts);
 
   fun cons_tr' (*"op #"*) [c, cs] =
-        const "_String" $ free (ssquote (implode (dest_char c :: dest_string cs)))
+        Syntax.const "_String" $
+          Syntax.free (Syntax.implode_xstr (dest_char c :: dest_string cs))
     | cons_tr' (*"op #"*) ts = raise Match;
 
 in
   val parse_translation = [("_Char", char_tr), ("_String", string_tr)];
   val print_translation = [("Char", char_tr'), ("op #", cons_tr')];
 end;
-