# HG changeset patch
# User wenzelm
# Date 921687534 -3600
# Node ID 5abd0d044adfd36858d586d3406a2052ec82f9e0
# Parent  3d9fd50fcc43b04a4299601dc905613e7e82184e
xstr token class;

diff -r 3d9fd50fcc43 -r 5abd0d044adf src/HOL/String.thy
--- a/src/HOL/String.thy	Wed Mar 17 16:53:46 1999 +0100
+++ b/src/HOL/String.thy	Wed Mar 17 17:18:54 1999 +0100
@@ -29,6 +29,9 @@
 
   (* chars *)
 
+  fun syntax_xstr x = Syntax.const "_xstr" $ Syntax.free x;
+
+
   val zero = ord "0";
   val ten = ord "A" - 10;
 
@@ -58,7 +61,7 @@
     | char_tr (*"_Char"*) ts = raise TERM ("char_tr", ts);
 
   fun char_tr' (*"Char"*) [t1, t2] =
-        Syntax.const "_Char" $ Syntax.free (Syntax.implode_xstr [dest_nibs t1 t2])
+        Syntax.const "_Char" $ syntax_xstr (Syntax.implode_xstr [dest_nibs t1 t2])
     | char_tr' (*"Char"*) _ = raise Match;
 
 
@@ -78,7 +81,7 @@
 
   fun cons_tr' (*"op #"*) [c, cs] =
         Syntax.const "_String" $
-          Syntax.free (Syntax.implode_xstr (dest_char c :: dest_string cs))
+          syntax_xstr (Syntax.implode_xstr (dest_char c :: dest_string cs))
     | cons_tr' (*"op #"*) ts = raise Match;
 
 in