1.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer_fact_filter.ML	Tue Aug 24 15:29:13 2010 +0200
     1.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_fact_filter.ML	Tue Aug 24 16:24:11 2010 +0200
     1.3 @@ -13,7 +13,8 @@
     1.4    val trace : bool Unsynchronized.ref
     1.5    val chained_prefix : string
     1.6    val name_thms_pair_from_ref :
     1.7 -    Proof.context -> thm list -> Facts.ref -> string * thm list
     1.8 +    Proof.context -> unit Symtab.table -> thm list -> Facts.ref
     1.9 +    -> string * thm list
    1.10    val relevant_facts :
    1.11      bool -> real -> real -> bool -> int -> bool -> relevance_override
    1.12      -> Proof.context * (thm list * 'a) -> term list -> term
    1.13 @@ -39,12 +40,13 @@
    1.14  (* Used to label theorems chained into the goal. *)
    1.15  val chained_prefix = sledgehammer_prefix ^ "chained_"
    1.16  
    1.17 -fun name_thms_pair_from_ref ctxt chained_ths xref =
    1.18 +fun name_thms_pair_from_ref ctxt reserved chained_ths xref =
    1.19    let
    1.20      val ths = ProofContext.get_fact ctxt xref
    1.21      val name = Facts.string_of_ref xref
    1.22 -               |> forall (member Thm.eq_thm chained_ths) ths
    1.23 -                  ? prefix chained_prefix
    1.24 +    val name = name |> Symtab.defined reserved name ? quote
    1.25 +                    |> forall (member Thm.eq_thm chained_ths) ths
    1.26 +                       ? prefix chained_prefix
    1.27    in (name, ths) end
    1.28  
    1.29  
    1.30 @@ -532,7 +534,7 @@
    1.31      is_strange_theorem thm
    1.32    end
    1.33  
    1.34 -fun all_name_thms_pairs ctxt full_types add_thms chained_ths =
    1.35 +fun all_name_thms_pairs ctxt reserved full_types add_thms chained_ths =
    1.36    let
    1.37      val global_facts = PureThy.facts_of (ProofContext.theory_of ctxt);
    1.38      val local_facts = ProofContext.facts_of ctxt
    1.39 @@ -564,18 +566,19 @@
    1.40              val ths =
    1.41                ths0 |> filter ((not o is_theorem_bad_for_atps full_types) orf
    1.42                                member Thm.eq_thm add_thms)
    1.43 +            fun backquotify th =
    1.44 +              "`" ^ Print_Mode.setmp [Print_Mode.input]
    1.45 +                                 (Syntax.string_of_term ctxt) (prop_of th) ^ "`"
    1.46              val name' =
    1.47                case find_first check_thms [name1, name2, name] of
    1.48 -                SOME name' => name'
    1.49 -              | NONE =>
    1.50 -                ths |> map (fn th =>
    1.51 -                               "`" ^ Print_Mode.setmp [Print_Mode.input]
    1.52 -                                         (Syntax.string_of_term ctxt)
    1.53 -                                         (prop_of th) ^ "`")
    1.54 -                    |> space_implode " "
    1.55 +                SOME name' => name' |> Symtab.defined reserved name' ? quote
    1.56 +              | NONE => ths |> map_filter (try backquotify) |> space_implode " "
    1.57            in
    1.58 -            cons (name' |> forall (member Thm.eq_thm chained_ths) ths0
    1.59 -                           ? prefix chained_prefix, ths)
    1.60 +            if name' = "" then
    1.61 +              I
    1.62 +            else
    1.63 +              cons (name' |> forall (member Thm.eq_thm chained_ths) ths0
    1.64 +                             ? prefix chained_prefix, ths)
    1.65            end)
    1.66    in
    1.67      [] |> add_valid_facts fold local_facts (unnamed_locals @ named_locals)
    1.68 @@ -609,9 +612,10 @@
    1.69                     (ctxt, (chained_ths, _)) hyp_ts concl_t =
    1.70    let
    1.71      val add_thms = maps (ProofContext.get_fact ctxt) add
    1.72 +    val reserved = reserved_isar_keyword_table ()
    1.73      val axioms =
    1.74 -      (if only then map (name_thms_pair_from_ref ctxt chained_ths) add
    1.75 -       else all_name_thms_pairs ctxt full_types add_thms chained_ths)
    1.76 +      (if only then map (name_thms_pair_from_ref ctxt reserved chained_ths) add
    1.77 +       else all_name_thms_pairs ctxt reserved full_types add_thms chained_ths)
    1.78        |> name_thm_pairs ctxt (respect_no_atp andalso not only)
    1.79        |> make_unique
    1.80    in

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

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

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