# HG changeset patch
# User blanchet
# Date 1271667720 -7200
# Node ID 3abbae8a10cd6550819c2be6f1ef62adc414d55f
# Parent  f3655a3ae1ab8673994aa3f6fed55980c07c42d0
allow "_" in TPTP names in debug mode

diff -r f3655a3ae1ab -r 3abbae8a10cd src/HOL/Tools/Sledgehammer/sledgehammer_fol_clause.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_fol_clause.ML	Mon Apr 19 10:45:08 2010 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_fol_clause.ML	Mon Apr 19 11:02:00 2010 +0200
@@ -251,7 +251,8 @@
       (s' |> rev
           |> implode
           |> String.translate
-                 (fn c => if Char.isAlphaNum c then String.str c else ""))
+                 (fn c => if Char.isAlphaNum c orelse c = #"_" then String.str c
+                          else ""))
       ^ replicate_string (String.size s - length s') "_"
     val s' =
       if s' = "" orelse not (Char.isAlpha (String.sub (s', 0))) then "X" ^ s'