# HG changeset patch
# User blanchet
# Date 1357322449 -3600
# Node ID b422a48adc2d7b199bd007cf36d56705bb909216
# Parent  69d2401954243b9bb24ba94350300ed9a7be3ab0
speed up generation of local theorem nicknames

diff -r 69d240195424 -r b422a48adc2d src/HOL/Tools/Sledgehammer/sledgehammer_mash.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_mash.ML	Fri Jan 04 19:00:49 2013 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_mash.ML	Fri Jan 04 19:00:49 2013 +0100
@@ -307,7 +307,7 @@
 
 local
 
-val version = "*** MaSh version 20121227a ***"
+val version = "*** MaSh version 20130104a ***"
 
 exception Too_New of unit
 
@@ -401,29 +401,25 @@
 
 (*** Isabelle helpers ***)
 
-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
 
-val local_prefix = "local" ^ Long_Name.separator
+fun elided_backquote_thm threshold th =
+  elide_string threshold
+    (backquote_thm (Proof_Context.init_global (Thm.theory_of_thm th)) th)
 
 fun nickname_of_thm th =
   if Thm.has_name_hint th then
     let val hint = Thm.get_name_hint th in
-      (* FIXME: There must be a better way to detect local facts. *)
+      (* There must be a better way to detect local facts. *)
       case try (unprefix local_prefix) hint of
         SOME suf =>
-        parent_of_local_thm th ^ Long_Name.separator ^ Long_Name.separator ^ suf
+        Context.theory_name (Thm.theory_of_thm th) ^ Long_Name.separator ^
+        Long_Name.separator ^ suf ^ Long_Name.separator ^
+        elided_backquote_thm 50 th
       | NONE => hint
     end
   else
-    backquote_thm (Proof_Context.init_global (Thm.theory_of_thm th)) th
+    elided_backquote_thm 200 th
 
 fun find_suggested_facts suggs facts =
   let
@@ -486,10 +482,8 @@
 val skos_feature = ("skos", 2.0 (* FUDGE *))
 
 fun theory_ord p =
-  if Theory.eq_thy p then
-    EQUAL
-  else if Theory.subthy p then
-    LESS
+  if Theory.subthy p then
+    if Theory.eq_thy p then EQUAL else LESS
   else if Theory.subthy (swap p) then
     GREATER
   else case int_ord (pairself (length o Theory.ancestors_of) p) of