Mercurial Mercurial > repos > isabelle / changeset
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | raw | gz | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
reverted e31e3f0071d4 because "foo.bar(5)" (with quotes) is wrong
authorblanchet
Fri, 29 Oct 2010 10:40:36 +0200
changeset 40251 63405dd65b0d
parent 40250 8792b0b89dcf
child 40252 029400b6c893
reverted e31e3f0071d4 because "foo.bar(5)" (with quotes) is wrong
src/HOL/Tools/Sledgehammer/sledgehammer_filter.ML file | annotate | diff | comparison | revisions 
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_filter.ML	Fri Oct 29 10:14:49 2010 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_filter.ML	Fri Oct 29 10:40:36 2010 +0200
@@ -87,8 +87,8 @@
 val theory_const_suffix = Long_Name.separator ^ " 1"
 
 fun needs_quoting reserved s =
-  Symtab.defined reserved s orelse
-  exists (not o Syntax.is_identifier) (Long_Name.explode s)
+  Symtab.defined reserved s (* FIXME: orelse
+  exists (not o Syntax.is_identifier) (Long_Name.explode s) *)
 
 fun repair_name reserved multi j name =
   (name |> needs_quoting reserved name ? quote) ^
isabelle