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_filter.ML
changeset 42290 b1f544c84040
parent 41999 3c029ef9e0f2
child 42358 b47d41d9f4b5 
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_filter.ML	Fri Apr 08 15:48:14 2011 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_filter.ML	Fri Apr 08 16:34:14 2011 +0200
@@ -99,7 +99,7 @@
 
 fun needs_quoting reserved s =
   Symtab.defined reserved s orelse
-  exists (not o Syntax.is_identifier) (Long_Name.explode s)
+  exists (not o Lexicon.is_identifier) (Long_Name.explode s)
 
 fun make_name reserved multi j name =
   (name |> needs_quoting reserved name ? quote) ^
isabelle