src/HOL/String.thy
changeset 6395 5abd0d044adf
parent 5121 5c1f89ae8aef
child 7224 e41e64476f9b
     1.1 --- a/src/HOL/String.thy	Wed Mar 17 16:53:46 1999 +0100
     1.2 +++ b/src/HOL/String.thy	Wed Mar 17 17:18:54 1999 +0100
     1.3 @@ -29,6 +29,9 @@
     1.4  
     1.5    (* chars *)
     1.6  
     1.7 +  fun syntax_xstr x = Syntax.const "_xstr" $ Syntax.free x;
     1.8 +
     1.9 +
    1.10    val zero = ord "0";
    1.11    val ten = ord "A" - 10;
    1.12  
    1.13 @@ -58,7 +61,7 @@
    1.14      | char_tr (*"_Char"*) ts = raise TERM ("char_tr", ts);
    1.15  
    1.16    fun char_tr' (*"Char"*) [t1, t2] =
    1.17 -        Syntax.const "_Char" $ Syntax.free (Syntax.implode_xstr [dest_nibs t1 t2])
    1.18 +        Syntax.const "_Char" $ syntax_xstr (Syntax.implode_xstr [dest_nibs t1 t2])
    1.19      | char_tr' (*"Char"*) _ = raise Match;
    1.20  
    1.21  
    1.22 @@ -78,7 +81,7 @@
    1.23  
    1.24    fun cons_tr' (*"op #"*) [c, cs] =
    1.25          Syntax.const "_String" $
    1.26 -          Syntax.free (Syntax.implode_xstr (dest_char c :: dest_string cs))
    1.27 +          syntax_xstr (Syntax.implode_xstr (dest_char c :: dest_string cs))
    1.28      | cons_tr' (*"op #"*) ts = raise Match;
    1.29  
    1.30  in