src/HOL/Tools/Sledgehammer/metis_clauses.ML
changeset 38738 0ce517c1970f
parent 38653 78d0f18d5b36
child 38748 69fea359d3f8
     1.1 --- a/src/HOL/Tools/Sledgehammer/metis_clauses.ML	Tue Aug 24 21:40:03 2010 +0200
     1.2 +++ b/src/HOL/Tools/Sledgehammer/metis_clauses.ML	Tue Aug 24 22:57:22 2010 +0200
     1.3 @@ -121,7 +121,7 @@
     1.4    Alphanumeric characters are left unchanged.
     1.5    The character _ goes to __
     1.6    Characters in the range ASCII space to / go to _A to _P, respectively.
     1.7 -  Other printing characters go to _nnn where nnn is the decimal ASCII code.*)
     1.8 +  Other characters go to _nnn where nnn is the decimal ASCII code.*)
     1.9  val A_minus_space = Char.ord #"A" - Char.ord #" ";
    1.10  
    1.11  fun stringN_of_int 0 _ = ""
    1.12 @@ -132,9 +132,7 @@
    1.13    else if c = #"_" then "__"
    1.14    else if #" " <= c andalso c <= #"/"
    1.15         then "_" ^ String.str (Char.chr (Char.ord c + A_minus_space))
    1.16 -  else if Char.isPrint c
    1.17 -       then ("_" ^ stringN_of_int 3 (Char.ord c))  (*fixed width, in case more digits follow*)
    1.18 -  else ""
    1.19 +  else ("_" ^ stringN_of_int 3 (Char.ord c))  (*fixed width, in case more digits follow*)
    1.20  
    1.21  val ascii_of = String.translate ascii_of_c;
    1.22