# HG changeset patch
# User blanchet
# Date 1288262004 -7200
# Node ID e31e3f0071d4023b15de0fd5bb6a8eb336ed6c6b
# Parent  dfa0d94991e47fa8ce1a1e3345a3c70b31328d47
support non-identifier-like fact names in Sledgehammer (e.g., "my lemma") by quoting them

diff -r dfa0d94991e4 -r e31e3f0071d4 src/HOL/Tools/Sledgehammer/sledgehammer_filter.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_filter.ML	Thu Oct 28 10:38:29 2010 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_filter.ML	Thu Oct 28 12:33:24 2010 +0200
@@ -86,8 +86,12 @@
 val skolem_prefix = sledgehammer_prefix ^ "sko"
 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)
+
 fun repair_name reserved multi j name =
-  (name |> Symtab.defined reserved name ? quote) ^
+  (name |> needs_quoting reserved name ? quote) ^
   (if multi then "(" ^ Int.toString j ^ ")" else "")
 
 fun fact_from_ref ctxt reserved chained_ths (xthm as (xref, args)) =