| changeset 43845 | d89353d17f54 |
| parent 42290 | b1f544c84040 |
| child 50238 | 98d35a7368bd |
--- a/src/Pure/ML/ml_syntax.ML Sat Jul 16 16:51:12 2011 +0200 +++ b/src/Pure/ML/ml_syntax.ML Sat Jul 16 17:11:49 2011 +0200 @@ -64,6 +64,7 @@ else if s = "\\" then "\\\\" else if s = "\t" then "\\t" else if s = "\n" then "\\n" + else if s = "\f" then "\\f" else if s = "\r" then "\\r" else let val c = ord s in