diff -r 76a2e506c125 -r cd1fcda1ea88 src/HOL/Tools/ATP/atp_proof_reconstruct.ML
--- a/src/HOL/Tools/ATP/atp_proof_reconstruct.ML	Thu Jan 03 15:13:11 2013 +0100
+++ b/src/HOL/Tools/ATP/atp_proof_reconstruct.ML	Thu Jan 03 17:10:12 2013 +0100
@@ -131,7 +131,7 @@
 fun repair_var_name s =
   let
     fun subscript_name s n = s ^ nat_subscript n
-    val s = String.map Char.toLower s
+    val s = s |> String.map Char.toLower
   in
     case space_explode "_" s of
       [_] => (case take_suffix Char.isDigit (String.explode s) of