src/HOL/Tools/Sledgehammer/sledgehammer_fol_clause.ML
changeset 36221 3abbae8a10cd
parent 36218 0e4a01f3e7d3
child 36222 0e3e49bd658d
     1.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer_fol_clause.ML	Mon Apr 19 10:45:08 2010 +0200
     1.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_fol_clause.ML	Mon Apr 19 11:02:00 2010 +0200
     1.3 @@ -251,7 +251,8 @@
     1.4        (s' |> rev
     1.5            |> implode
     1.6            |> String.translate
     1.7 -                 (fn c => if Char.isAlphaNum c then String.str c else ""))
     1.8 +                 (fn c => if Char.isAlphaNum c orelse c = #"_" then String.str c
     1.9 +                          else ""))
    1.10        ^ replicate_string (String.size s - length s') "_"
    1.11      val s' =
    1.12        if s' = "" orelse not (Char.isAlpha (String.sub (s', 0))) then "X" ^ s'