# HG changeset patch
# User blanchet
# Date 1288341636 -7200
# Node ID 63405dd65b0d5dc8078d6817ee87affb1fa7a45a
# Parent  8792b0b89dcfede790e3c22f4e7d0e8646f4b2bc
reverted e31e3f0071d4 because "foo.bar(5)" (with quotes) is wrong

diff -r 8792b0b89dcf -r 63405dd65b0d src/HOL/Tools/Sledgehammer/sledgehammer_filter.ML
--- 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) ^