1.1 --- a/src/HOL/TPTP/mash_export.ML	Fri Jul 20 22:19:45 2012 +0200
     1.2 +++ b/src/HOL/TPTP/mash_export.ML	Fri Jul 20 22:19:45 2012 +0200
     1.3 @@ -32,7 +32,7 @@
     1.4    ths |> sort (thm_ord o swap o pairself snd)
     1.5        |> map (snd #> `(theory_of_thm #> Context.theory_name))
     1.6        |> AList.coalesce (op =)
     1.7 -      |> map (apsnd (map Thm.get_name_hint))
     1.8 +      |> map (apsnd (map nickname_of))
     1.9  
    1.10  fun has_thy thy th =
    1.11    Context.theory_name thy = Context.theory_name (theory_of_thm th)
    1.12 @@ -51,7 +51,7 @@
    1.13  
    1.14  val all_names =
    1.15    filter_out is_likely_tautology_or_too_meta
    1.16 -  #> map (rpair () o Thm.get_name_hint) #> Symtab.make
    1.17 +  #> map (rpair () o nickname_of) #> Symtab.make
    1.18  
    1.19  fun generate_accessibility thy include_thy file_name =
    1.20    let
    1.21 @@ -83,7 +83,7 @@
    1.22        |> not include_thy ? filter_out (has_thy thy o snd)
    1.23      fun do_fact ((_, (_, status)), th) =
    1.24        let
    1.25 -        val name = Thm.get_name_hint th
    1.26 +        val name = nickname_of th
    1.27          val feats =
    1.28            features_of ctxt prover (theory_of_thm th) status [prop_of th]
    1.29          val s = escape_meta name ^ ": " ^ escape_metas feats ^ "\n"
    1.30 @@ -101,7 +101,7 @@
    1.31      val all_names = all_names ths
    1.32      fun do_thm th =
    1.33        let
    1.34 -        val name = Thm.get_name_hint th
    1.35 +        val name = nickname_of th
    1.36          val deps = isabelle_dependencies_of all_names th
    1.37          val s = escape_meta name ^ ": " ^ escape_metas deps ^ "\n"
    1.38        in File.append path s end
    1.39 @@ -118,18 +118,17 @@
    1.40        |> not include_thy ? filter_out (has_thy thy o snd)
    1.41      val ths = facts |> map snd
    1.42      val all_names = all_names ths
    1.43 -    fun is_dep dep (_, th) = Thm.get_name_hint th = dep
    1.44 +    fun is_dep dep (_, th) = nickname_of th = dep
    1.45      fun add_isar_dep facts dep accum =
    1.46        if exists (is_dep dep) accum then
    1.47          accum
    1.48        else case find_first (is_dep dep) facts of
    1.49          SOME ((name, status), th) => accum @ [((name, status), th)]
    1.50        | NONE => accum (* shouldn't happen *)
    1.51 -    fun fix_name ((_, stature), th) =
    1.52 -      ((fn () => th |> Thm.get_name_hint, stature), th)
    1.53 +    fun fix_name ((_, stature), th) = ((fn () => nickname_of th, stature), th)
    1.54      fun do_thm th =
    1.55        let
    1.56 -        val name = Thm.get_name_hint th
    1.57 +        val name = nickname_of th
    1.58          val goal = goal_of_thm thy th
    1.59          val (_, hyp_ts, concl_t) = ATP_Util.strip_subgoal ctxt goal 1
    1.60          val deps =
    1.61 @@ -168,7 +167,7 @@
    1.62      val all_names = all_names ths
    1.63      fun do_fact ((_, (_, status)), th) prevs =
    1.64        let
    1.65 -        val name = Thm.get_name_hint th
    1.66 +        val name = nickname_of th
    1.67          val feats = features_of ctxt prover thy status [prop_of th]
    1.68          val deps = isabelle_dependencies_of all_names th
    1.69          val kind = Thm.legacy_get_kind th
    1.70 @@ -196,7 +195,7 @@
    1.71              |>> sort (thm_ord o pairself snd)
    1.72      fun do_fact (fact as (_, th)) old_facts =
    1.73        let
    1.74 -        val name = Thm.get_name_hint th
    1.75 +        val name = nickname_of th
    1.76          val goal = goal_of_thm thy th
    1.77          val (_, hyp_ts, concl_t) = ATP_Util.strip_subgoal ctxt goal 1
    1.78          val kind = Thm.legacy_get_kind th