--- 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'