src/HOL/Tools/Sledgehammer/sledgehammer_filter_mash.ML

   val escape_meta : string -> string
   val escape_metas : string list -> string
   val unescape_meta : string -> string
   val unescape_metas : string -> string list
   val extract_query : string -> string * string list
+  val nickname_of : thm -> string
   val suggested_facts : string list -> ('a * thm) list -> ('a * thm) list
   val mesh_facts :
     int -> (('a * thm) list * ('a * thm) list) list -> ('a * thm) list
   val is_likely_tautology_or_too_meta : thm -> bool
   val theory_ord : theory * theory -> order

 fun extract_query line =
   case space_explode ":" line of
     [goal_name, suggs] => (unescape_meta goal_name, unescape_metas suggs)
   | _ => ("", [])
 
+fun parent_of_local_thm th =
+  let
+    val thy = th |> Thm.theory_of_thm
+    val facts = thy |> Global_Theory.facts_of
+    val space = facts |> Facts.space_of
+    fun id_of s = #id (Name_Space.the_entry space s)
+    fun max_id (s', _) (s, id) =
+      let val id' = id_of s' in if id > id' then (s, id) else (s', id') end
+  in ("", ~1) |> Facts.fold_static max_id facts |> fst end
+
+val local_prefix = "local" ^ Long_Name.separator
+
+fun nickname_of th =
+  let val hint = Thm.get_name_hint th in
+    (* FIXME: There must be a better way to detect local facts. *)
+    case try (unprefix local_prefix) hint of
+      SOME suff =>
+      parent_of_local_thm th ^ Long_Name.separator ^ Long_Name.separator ^ suff
+    | NONE => hint
+  end
+
 fun suggested_facts suggs facts =
   let
-    fun add_fact (fact as (_, th)) = Symtab.default (Thm.get_name_hint th, fact)
+    fun add_fact (fact as (_, th)) = Symtab.default (nickname_of th, fact)
     val tab = Symtab.empty |> fold add_fact facts
   in map_filter (Symtab.lookup tab) suggs end
 
 (* Ad hoc score function roughly based on Blanchette's Ringberg 2011 data. *)
 fun score x = Math.pow (1.5, 15.5 - 0.05 * Real.fromInt x) + 15.0

 fun mash_can_suggest_facts ctxt =
   not (Graph.is_empty (#fact_graph (mash_get ctxt)))
 
 fun parents_wrt_facts facts fact_graph =
   let
-    val facts = [] |> fold (cons o Thm.get_name_hint o snd) facts
+    val facts = [] |> fold (cons o nickname_of o snd) facts
     val tab = Symtab.empty |> fold (fn name => Symtab.update (name, ())) facts
     fun insert_not_seen seen name =
       not (member (op =) seen name) ? insert (op =) name
-    fun parents_of seen parents [] = parents
+    fun parents_of _ parents [] = parents
       | parents_of seen parents (name :: names) =
         if Symtab.defined tab name then
           parents_of (name :: seen) (name :: parents) names
         else
           parents_of (name :: seen) parents

    later for various reasons and "meshing" gives better results with some
    slack. *)
 fun max_suggs_of max_facts = max_facts + Int.min (200, max_facts)
 
 fun is_fact_in_graph fact_graph (_, th) =
-  can (Graph.get_node fact_graph) (Thm.get_name_hint th)
+  can (Graph.get_node fact_graph) (nickname_of th)
 
 fun mash_suggest_facts ctxt ({overlord, ...} : params) prover max_facts hyp_ts
                        concl_t facts =
   let
     val thy = Proof_Context.theory_of ctxt

     else
       let
         val ths = facts |> map snd
         val all_names =
           ths |> filter_out is_likely_tautology_or_too_meta
-              |> map (rpair () o Thm.get_name_hint)
+              |> map (rpair () o nickname_of)
               |> Symtab.make
         fun trim_deps deps = if length deps > max_dependencies then [] else deps
         fun do_fact _ (accum as (_, true)) = accum
           | do_fact ((_, (_, status)), th) ((parents, upds), false) =
             let
-              val name = Thm.get_name_hint th
+              val name = nickname_of th
               val feats =
                 features_of ctxt prover (theory_of_thm th) status [prop_of th]
               val deps = isabelle_dependencies_of all_names th |> trim_deps
               val upd = (name, parents, feats, deps)
             in (([name], upd :: upds), timed_out pass1_learn_timeout_factor) end

   let
     val thy = Proof_Context.theory_of ctxt
     val prover = hd provers
     val name = ATP_Util.timestamp () ^ " " ^ serial_string () (* fresh enough *)
     val feats = features_of ctxt prover thy General [t]
-    val deps = used_ths |> map Thm.get_name_hint
+    val deps = used_ths |> map nickname_of
   in
     mash_map ctxt (fn {thys, fact_graph} =>
         let
           val parents = parents_wrt_facts facts fact_graph
           val upds = [(name, parents, feats, deps)]