1.1 --- a/src/HOL/TPTP/mash_eval.ML	Fri Jul 20 22:19:45 2012 +0200
     1.2 +++ b/src/HOL/TPTP/mash_eval.ML	Fri Jul 20 22:19:45 2012 +0200
     1.3 @@ -28,7 +28,7 @@
     1.4  
     1.5  val all_names =
     1.6    filter_out is_likely_tautology_or_too_meta
     1.7 -  #> map (rpair () o Thm.get_name_hint) #> Symtab.make
     1.8 +  #> map (rpair () o nickname_of) #> Symtab.make
     1.9  
    1.10  fun evaluate_mash_suggestions ctxt params thy file_name =
    1.11    let
    1.12 @@ -70,7 +70,7 @@
    1.13        let
    1.14          val (name, suggs) = extract_query line
    1.15          val th =
    1.16 -          case find_first (fn (_, th) => Thm.get_name_hint th = name) facts of
    1.17 +          case find_first (fn (_, th) => nickname_of th = name) facts of
    1.18              SOME (_, th) => th
    1.19            | NONE => error ("No fact called \"" ^ name ^ "\"")
    1.20          val goal = goal_of_thm thy th

     2.1 --- a/src/HOL/TPTP/mash_export.ML	Fri Jul 20 22:19:45 2012 +0200
     2.2 +++ b/src/HOL/TPTP/mash_export.ML	Fri Jul 20 22:19:45 2012 +0200
     2.3 @@ -32,7 +32,7 @@
     2.4    ths |> sort (thm_ord o swap o pairself snd)
     2.5        |> map (snd #> `(theory_of_thm #> Context.theory_name))
     2.6        |> AList.coalesce (op =)
     2.7 -      |> map (apsnd (map Thm.get_name_hint))
     2.8 +      |> map (apsnd (map nickname_of))
     2.9  
    2.10  fun has_thy thy th =
    2.11    Context.theory_name thy = Context.theory_name (theory_of_thm th)
    2.12 @@ -51,7 +51,7 @@
    2.13  
    2.14  val all_names =
    2.15    filter_out is_likely_tautology_or_too_meta
    2.16 -  #> map (rpair () o Thm.get_name_hint) #> Symtab.make
    2.17 +  #> map (rpair () o nickname_of) #> Symtab.make
    2.18  
    2.19  fun generate_accessibility thy include_thy file_name =
    2.20    let
    2.21 @@ -83,7 +83,7 @@
    2.22        |> not include_thy ? filter_out (has_thy thy o snd)
    2.23      fun do_fact ((_, (_, status)), th) =
    2.24        let
    2.25 -        val name = Thm.get_name_hint th
    2.26 +        val name = nickname_of th
    2.27          val feats =
    2.28            features_of ctxt prover (theory_of_thm th) status [prop_of th]
    2.29          val s = escape_meta name ^ ": " ^ escape_metas feats ^ "\n"
    2.30 @@ -101,7 +101,7 @@
    2.31      val all_names = all_names ths
    2.32      fun do_thm th =
    2.33        let
    2.34 -        val name = Thm.get_name_hint th
    2.35 +        val name = nickname_of th
    2.36          val deps = isabelle_dependencies_of all_names th
    2.37          val s = escape_meta name ^ ": " ^ escape_metas deps ^ "\n"
    2.38        in File.append path s end
    2.39 @@ -118,18 +118,17 @@
    2.40        |> not include_thy ? filter_out (has_thy thy o snd)
    2.41      val ths = facts |> map snd
    2.42      val all_names = all_names ths
    2.43 -    fun is_dep dep (_, th) = Thm.get_name_hint th = dep
    2.44 +    fun is_dep dep (_, th) = nickname_of th = dep
    2.45      fun add_isar_dep facts dep accum =
    2.46        if exists (is_dep dep) accum then
    2.47          accum
    2.48        else case find_first (is_dep dep) facts of
    2.49          SOME ((name, status), th) => accum @ [((name, status), th)]
    2.50        | NONE => accum (* shouldn't happen *)
    2.51 -    fun fix_name ((_, stature), th) =
    2.52 -      ((fn () => th |> Thm.get_name_hint, stature), th)
    2.53 +    fun fix_name ((_, stature), th) = ((fn () => nickname_of th, stature), th)
    2.54      fun do_thm th =
    2.55        let
    2.56 -        val name = Thm.get_name_hint th
    2.57 +        val name = nickname_of th
    2.58          val goal = goal_of_thm thy th
    2.59          val (_, hyp_ts, concl_t) = ATP_Util.strip_subgoal ctxt goal 1
    2.60          val deps =
    2.61 @@ -168,7 +167,7 @@
    2.62      val all_names = all_names ths
    2.63      fun do_fact ((_, (_, status)), th) prevs =
    2.64        let
    2.65 -        val name = Thm.get_name_hint th
    2.66 +        val name = nickname_of th
    2.67          val feats = features_of ctxt prover thy status [prop_of th]
    2.68          val deps = isabelle_dependencies_of all_names th
    2.69          val kind = Thm.legacy_get_kind th
    2.70 @@ -196,7 +195,7 @@
    2.71              |>> sort (thm_ord o pairself snd)
    2.72      fun do_fact (fact as (_, th)) old_facts =
    2.73        let
    2.74 -        val name = Thm.get_name_hint th
    2.75 +        val name = nickname_of th
    2.76          val goal = goal_of_thm thy th
    2.77          val (_, hyp_ts, concl_t) = ATP_Util.strip_subgoal ctxt goal 1
    2.78          val kind = Thm.legacy_get_kind th

     3.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer_filter_mash.ML	Fri Jul 20 22:19:45 2012 +0200
     3.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_filter_mash.ML	Fri Jul 20 22:19:45 2012 +0200
     3.3 @@ -25,6 +25,7 @@
     3.4    val unescape_meta : string -> string
     3.5    val unescape_metas : string -> string list
     3.6    val extract_query : string -> string * string list
     3.7 +  val nickname_of : thm -> string
     3.8    val suggested_facts : string list -> ('a * thm) list -> ('a * thm) list
     3.9    val mesh_facts :
    3.10      int -> (('a * thm) list * ('a * thm) list) list -> ('a * thm) list
    3.11 @@ -122,9 +123,30 @@
    3.12      [goal_name, suggs] => (unescape_meta goal_name, unescape_metas suggs)
    3.13    | _ => ("", [])
    3.14  
    3.15 +fun parent_of_local_thm th =
    3.16 +  let
    3.17 +    val thy = th |> Thm.theory_of_thm
    3.18 +    val facts = thy |> Global_Theory.facts_of
    3.19 +    val space = facts |> Facts.space_of
    3.20 +    fun id_of s = #id (Name_Space.the_entry space s)
    3.21 +    fun max_id (s', _) (s, id) =
    3.22 +      let val id' = id_of s' in if id > id' then (s, id) else (s', id') end
    3.23 +  in ("", ~1) |> Facts.fold_static max_id facts |> fst end
    3.24 +
    3.25 +val local_prefix = "local" ^ Long_Name.separator
    3.26 +
    3.27 +fun nickname_of th =
    3.28 +  let val hint = Thm.get_name_hint th in
    3.29 +    (* FIXME: There must be a better way to detect local facts. *)
    3.30 +    case try (unprefix local_prefix) hint of
    3.31 +      SOME suff =>
    3.32 +      parent_of_local_thm th ^ Long_Name.separator ^ Long_Name.separator ^ suff
    3.33 +    | NONE => hint
    3.34 +  end
    3.35 +
    3.36  fun suggested_facts suggs facts =
    3.37    let
    3.38 -    fun add_fact (fact as (_, th)) = Symtab.default (Thm.get_name_hint th, fact)
    3.39 +    fun add_fact (fact as (_, th)) = Symtab.default (nickname_of th, fact)
    3.40      val tab = Symtab.empty |> fold add_fact facts
    3.41    in map_filter (Symtab.lookup tab) suggs end
    3.42  
    3.43 @@ -468,11 +490,11 @@
    3.44  
    3.45  fun parents_wrt_facts facts fact_graph =
    3.46    let
    3.47 -    val facts = [] |> fold (cons o Thm.get_name_hint o snd) facts
    3.48 +    val facts = [] |> fold (cons o nickname_of o snd) facts
    3.49      val tab = Symtab.empty |> fold (fn name => Symtab.update (name, ())) facts
    3.50      fun insert_not_seen seen name =
    3.51        not (member (op =) seen name) ? insert (op =) name
    3.52 -    fun parents_of seen parents [] = parents
    3.53 +    fun parents_of _ parents [] = parents
    3.54        | parents_of seen parents (name :: names) =
    3.55          if Symtab.defined tab name then
    3.56            parents_of (name :: seen) (name :: parents) names
    3.57 @@ -488,7 +510,7 @@
    3.58  fun max_suggs_of max_facts = max_facts + Int.min (200, max_facts)
    3.59  
    3.60  fun is_fact_in_graph fact_graph (_, th) =
    3.61 -  can (Graph.get_node fact_graph) (Thm.get_name_hint th)
    3.62 +  can (Graph.get_node fact_graph) (nickname_of th)
    3.63  
    3.64  fun mash_suggest_facts ctxt ({overlord, ...} : params) prover max_facts hyp_ts
    3.65                         concl_t facts =
    3.66 @@ -545,13 +567,13 @@
    3.67          val ths = facts |> map snd
    3.68          val all_names =
    3.69            ths |> filter_out is_likely_tautology_or_too_meta
    3.70 -              |> map (rpair () o Thm.get_name_hint)
    3.71 +              |> map (rpair () o nickname_of)
    3.72                |> Symtab.make
    3.73          fun trim_deps deps = if length deps > max_dependencies then [] else deps
    3.74          fun do_fact _ (accum as (_, true)) = accum
    3.75            | do_fact ((_, (_, status)), th) ((parents, upds), false) =
    3.76              let
    3.77 -              val name = Thm.get_name_hint th
    3.78 +              val name = nickname_of th
    3.79                val feats =
    3.80                  features_of ctxt prover (theory_of_thm th) status [prop_of th]
    3.81                val deps = isabelle_dependencies_of all_names th |> trim_deps
    3.82 @@ -591,7 +613,7 @@
    3.83      val prover = hd provers
    3.84      val name = ATP_Util.timestamp () ^ " " ^ serial_string () (* fresh enough *)
    3.85      val feats = features_of ctxt prover thy General [t]
    3.86 -    val deps = used_ths |> map Thm.get_name_hint
    3.87 +    val deps = used_ths |> map nickname_of
    3.88    in
    3.89      mash_map ctxt (fn {thys, fact_graph} =>
    3.90          let