quote facts whose names collide with a keyword or command name (cf. "subclass" in "Jinja/J/TypeSafe.thy")

--- a/src/HOL/Tools/Sledgehammer/sledgehammer_fact_filter.ML	Tue Aug 24 15:29:13 2010 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_fact_filter.ML	Tue Aug 24 16:24:11 2010 +0200
@@ -13,7 +13,8 @@
   val trace : bool Unsynchronized.ref
   val chained_prefix : string
   val name_thms_pair_from_ref :
-    Proof.context -> thm list -> Facts.ref -> string * thm list
+    Proof.context -> unit Symtab.table -> thm list -> Facts.ref
+    -> string * thm list
   val relevant_facts :
     bool -> real -> real -> bool -> int -> bool -> relevance_override
     -> Proof.context * (thm list * 'a) -> term list -> term
@@ -39,12 +40,13 @@
 (* Used to label theorems chained into the goal. *)
 val chained_prefix = sledgehammer_prefix ^ "chained_"
 
-fun name_thms_pair_from_ref ctxt chained_ths xref =
+fun name_thms_pair_from_ref ctxt reserved chained_ths xref =
   let
     val ths = ProofContext.get_fact ctxt xref
     val name = Facts.string_of_ref xref
-               |> forall (member Thm.eq_thm chained_ths) ths
-                  ? prefix chained_prefix
+    val name = name |> Symtab.defined reserved name ? quote
+                    |> forall (member Thm.eq_thm chained_ths) ths
+                       ? prefix chained_prefix
   in (name, ths) end
 
 
@@ -532,7 +534,7 @@
     is_strange_theorem thm
   end
 
-fun all_name_thms_pairs ctxt full_types add_thms chained_ths =
+fun all_name_thms_pairs ctxt reserved full_types add_thms chained_ths =
   let
     val global_facts = PureThy.facts_of (ProofContext.theory_of ctxt);
     val local_facts = ProofContext.facts_of ctxt
@@ -564,18 +566,19 @@
             val ths =
               ths0 |> filter ((not o is_theorem_bad_for_atps full_types) orf
                               member Thm.eq_thm add_thms)
+            fun backquotify th =
+              "`" ^ Print_Mode.setmp [Print_Mode.input]
+                                 (Syntax.string_of_term ctxt) (prop_of th) ^ "`"
             val name' =
               case find_first check_thms [name1, name2, name] of
-                SOME name' => name'
-              | NONE =>
-                ths |> map (fn th =>
-                               "`" ^ Print_Mode.setmp [Print_Mode.input]
-                                         (Syntax.string_of_term ctxt)
-                                         (prop_of th) ^ "`")
-                    |> space_implode " "
+                SOME name' => name' |> Symtab.defined reserved name' ? quote
+              | NONE => ths |> map_filter (try backquotify) |> space_implode " "
           in
-            cons (name' |> forall (member Thm.eq_thm chained_ths) ths0
-                           ? prefix chained_prefix, ths)
+            if name' = "" then
+              I
+            else
+              cons (name' |> forall (member Thm.eq_thm chained_ths) ths0
+                             ? prefix chained_prefix, ths)
           end)
   in
     [] |> add_valid_facts fold local_facts (unnamed_locals @ named_locals)
@@ -609,9 +612,10 @@
                    (ctxt, (chained_ths, _)) hyp_ts concl_t =
   let
     val add_thms = maps (ProofContext.get_fact ctxt) add
+    val reserved = reserved_isar_keyword_table ()
     val axioms =
-      (if only then map (name_thms_pair_from_ref ctxt chained_ths) add
-       else all_name_thms_pairs ctxt full_types add_thms chained_ths)
+      (if only then map (name_thms_pair_from_ref ctxt reserved chained_ths) add
+       else all_name_thms_pairs ctxt reserved full_types add_thms chained_ths)
       |> name_thm_pairs ctxt (respect_no_atp andalso not only)
       |> make_unique
   in

--- a/src/HOL/Tools/Sledgehammer/sledgehammer_fact_minimize.ML	Tue Aug 24 15:29:13 2010 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_fact_minimize.ML	Tue Aug 24 16:24:11 2010 +0200
@@ -157,8 +157,10 @@
 fun run_minimize params i refs state =
   let
     val ctxt = Proof.context_of state
+    val reserved = reserved_isar_keyword_table ()
     val chained_ths = #facts (Proof.goal state)
-    val name_thms_pairs = map (name_thms_pair_from_ref ctxt chained_ths) refs
+    val name_thms_pairs =
+      map (name_thms_pair_from_ref ctxt reserved chained_ths) refs
   in
     case subgoal_count state of
       0 => priority "No subgoal!"

--- a/src/HOL/Tools/Sledgehammer/sledgehammer_proof_reconstruct.ML	Tue Aug 24 15:29:13 2010 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_proof_reconstruct.ML	Tue Aug 24 16:24:11 2010 +0200
@@ -613,8 +613,8 @@
   "Try this command: " ^
   Markup.markup Markup.sendback (metis_command full_types i n ([], ss)) ^ "."
 fun minimize_line _ [] = ""
-  | minimize_line minimize_command facts =
-    case minimize_command facts of
+  | minimize_line minimize_command ss =
+    case minimize_command ss of
       "" => ""
     | command =>
       "\nTo minimize the number of lemmas, try this: " ^

--- a/src/HOL/Tools/Sledgehammer/sledgehammer_util.ML	Tue Aug 24 15:29:13 2010 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_util.ML	Tue Aug 24 16:24:11 2010 +0200
@@ -21,6 +21,7 @@
   val specialize_type : theory -> (string * typ) -> term -> term
   val subgoal_count : Proof.state -> int
   val strip_subgoal : thm -> int -> (string * typ) list * term list * term
+  val reserved_isar_keyword_table : unit -> unit Symtab.table
 end;
  
 structure Sledgehammer_Util : SLEDGEHAMMER_UTIL =
@@ -155,4 +156,8 @@
     val concl_t = t |> Logic.strip_assums_concl |> curry subst_bounds frees
   in (rev (map dest_Free frees), hyp_ts, concl_t) end
 
+fun reserved_isar_keyword_table () =
+  union (op =) (Keyword.dest_keywords ()) (Keyword.dest_commands ())
+  |> map (rpair ()) |> Symtab.make
+
 end;