# HG changeset patch
# User wenzelm
# Date 1236088452 -3600
# Node ID 0300b7420b07b78a5814c116d4066b5b418fc1f1
# Parent  47cce3d47e629f551432d4cfb86506cb65fd2680
nicer_shortest: use NameSpace.extern_flags with disabled "features" instead of internal NameSpace.get_accesses;

diff -r 47cce3d47e62 -r 0300b7420b07 src/Pure/Tools/find_theorems.ML
--- a/src/Pure/Tools/find_theorems.ML	Tue Mar 03 14:53:29 2009 +0100
+++ b/src/Pure/Tools/find_theorems.ML	Tue Mar 03 14:54:12 2009 +0100
@@ -306,14 +306,11 @@
 
 fun nicer_shortest ctxt =
   let
-    val ns = ProofContext.theory_of ctxt
-             |> PureThy.facts_of
-             |> Facts.space_of;
+    (* FIXME global name space!? *)
+    val space = Facts.space_of (PureThy.facts_of (ProofContext.theory_of ctxt));
 
-    val len_sort = sort (int_ord o (pairself size));
-    fun shorten s = (case len_sort (NameSpace.get_accesses ns s) of
-                       [] => s
-                     | s'::_ => s');
+    val shorten =
+      NameSpace.extern_flags {long_names = false, short_names = false, unique_names = false} space;
 
     fun nicer (Facts.Named ((x, _), i)) (Facts.Named ((y, _), j)) =
           nicer_name (shorten x, i) (shorten y, j)