1.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer_filter_mash.ML	Fri Jul 20 22:19:45 2012 +0200
     1.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_filter_mash.ML	Fri Jul 20 22:19:45 2012 +0200
     1.3 @@ -25,6 +25,7 @@
     1.4    val unescape_meta : string -> string
     1.5    val unescape_metas : string -> string list
     1.6    val extract_query : string -> string * string list
     1.7 +  val nickname_of : thm -> string
     1.8    val suggested_facts : string list -> ('a * thm) list -> ('a * thm) list
     1.9    val mesh_facts :
    1.10      int -> (('a * thm) list * ('a * thm) list) list -> ('a * thm) list
    1.11 @@ -122,9 +123,30 @@
    1.12      [goal_name, suggs] => (unescape_meta goal_name, unescape_metas suggs)
    1.13    | _ => ("", [])
    1.14  
    1.15 +fun parent_of_local_thm th =
    1.16 +  let
    1.17 +    val thy = th |> Thm.theory_of_thm
    1.18 +    val facts = thy |> Global_Theory.facts_of
    1.19 +    val space = facts |> Facts.space_of
    1.20 +    fun id_of s = #id (Name_Space.the_entry space s)
    1.21 +    fun max_id (s', _) (s, id) =
    1.22 +      let val id' = id_of s' in if id > id' then (s, id) else (s', id') end
    1.23 +  in ("", ~1) |> Facts.fold_static max_id facts |> fst end
    1.24 +
    1.25 +val local_prefix = "local" ^ Long_Name.separator
    1.26 +
    1.27 +fun nickname_of th =
    1.28 +  let val hint = Thm.get_name_hint th in
    1.29 +    (* FIXME: There must be a better way to detect local facts. *)
    1.30 +    case try (unprefix local_prefix) hint of
    1.31 +      SOME suff =>
    1.32 +      parent_of_local_thm th ^ Long_Name.separator ^ Long_Name.separator ^ suff
    1.33 +    | NONE => hint
    1.34 +  end
    1.35 +
    1.36  fun suggested_facts suggs facts =
    1.37    let
    1.38 -    fun add_fact (fact as (_, th)) = Symtab.default (Thm.get_name_hint th, fact)
    1.39 +    fun add_fact (fact as (_, th)) = Symtab.default (nickname_of th, fact)
    1.40      val tab = Symtab.empty |> fold add_fact facts
    1.41    in map_filter (Symtab.lookup tab) suggs end
    1.42  
    1.43 @@ -468,11 +490,11 @@
    1.44  
    1.45  fun parents_wrt_facts facts fact_graph =
    1.46    let
    1.47 -    val facts = [] |> fold (cons o Thm.get_name_hint o snd) facts
    1.48 +    val facts = [] |> fold (cons o nickname_of o snd) facts
    1.49      val tab = Symtab.empty |> fold (fn name => Symtab.update (name, ())) facts
    1.50      fun insert_not_seen seen name =
    1.51        not (member (op =) seen name) ? insert (op =) name
    1.52 -    fun parents_of seen parents [] = parents
    1.53 +    fun parents_of _ parents [] = parents
    1.54        | parents_of seen parents (name :: names) =
    1.55          if Symtab.defined tab name then
    1.56            parents_of (name :: seen) (name :: parents) names
    1.57 @@ -488,7 +510,7 @@
    1.58  fun max_suggs_of max_facts = max_facts + Int.min (200, max_facts)
    1.59  
    1.60  fun is_fact_in_graph fact_graph (_, th) =
    1.61 -  can (Graph.get_node fact_graph) (Thm.get_name_hint th)
    1.62 +  can (Graph.get_node fact_graph) (nickname_of th)
    1.63  
    1.64  fun mash_suggest_facts ctxt ({overlord, ...} : params) prover max_facts hyp_ts
    1.65                         concl_t facts =
    1.66 @@ -545,13 +567,13 @@
    1.67          val ths = facts |> map snd
    1.68          val all_names =
    1.69            ths |> filter_out is_likely_tautology_or_too_meta
    1.70 -              |> map (rpair () o Thm.get_name_hint)
    1.71 +              |> map (rpair () o nickname_of)
    1.72                |> Symtab.make
    1.73          fun trim_deps deps = if length deps > max_dependencies then [] else deps
    1.74          fun do_fact _ (accum as (_, true)) = accum
    1.75            | do_fact ((_, (_, status)), th) ((parents, upds), false) =
    1.76              let
    1.77 -              val name = Thm.get_name_hint th
    1.78 +              val name = nickname_of th
    1.79                val feats =
    1.80                  features_of ctxt prover (theory_of_thm th) status [prop_of th]
    1.81                val deps = isabelle_dependencies_of all_names th |> trim_deps
    1.82 @@ -591,7 +613,7 @@
    1.83      val prover = hd provers
    1.84      val name = ATP_Util.timestamp () ^ " " ^ serial_string () (* fresh enough *)
    1.85      val feats = features_of ctxt prover thy General [t]
    1.86 -    val deps = used_ths |> map Thm.get_name_hint
    1.87 +    val deps = used_ths |> map nickname_of
    1.88    in
    1.89      mash_map ctxt (fn {thys, fact_graph} =>
    1.90          let