Mercurial Mercurial > repos > isabelle / diff
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | file | latest | revisions | annotate | diff | comparison | raw | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
src/HOL/Tools/Sledgehammer/sledgehammer_fol_clause.ML
changeset 36221 3abbae8a10cd
parent 36218 0e4a01f3e7d3
child 36222 0e3e49bd658d 
--- 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'
isabelle