# HG changeset patch
# User haftmann
# Date 1648919014 0
# Node ID a58718427bff6cafbd2bcbbd9f72b16b15c32378
# Parent  e852c776a455848472d09dd0e913597650ae79f2
tuned whitespace in generated code

diff -r e852c776a455 -r a58718427bff src/HOL/String.thy
--- a/src/HOL/String.thy	Fri Apr 01 16:41:16 2022 +0000
+++ b/src/HOL/String.thy	Sat Apr 02 17:03:34 2022 +0000
@@ -691,7 +691,7 @@
     and (Haskell) "map/ (let chr k | (0 <= k && k < 128) = Prelude.toEnum k :: Prelude.Char in chr . Prelude.fromInteger)"
     and (Scala) "\"\"/ ++/ _.map((k: BigInt) => if (BigInt(0) <= k && k < BigInt(128)) k.charValue else sys.error(\"Non-ASCII character in literal\"))"
 | constant String.asciis_of_literal \<rightharpoonup>
-    (SML) "!(List.map (fn c => let val k = Char.ord c in if k < 128 then IntInf.fromInt k else raise Fail \"Non-ASCII character in literal\" end) /o String.explode)"
+    (SML) "!(List.map (fn c => let val k = Char.ord c in if k < 128 then IntInf.fromInt k else raise Fail \"Non-ASCII character in literal\" end)/ o String.explode)"
     and (OCaml) "!(let s = _ in let rec exp i l = if i < 0 then l else exp (i - 1) (let k = Char.code (String.get s i) in
       if k < 128 then Z.of'_int k :: l else failwith \"Non-ASCII character in literal\") in exp (String.length s - 1) [])"
     and (Haskell) "map/ (let ord k | (k < 128) = Prelude.toInteger k in ord . (Prelude.fromEnum :: Prelude.Char -> Prelude.Int))"