nicer_shortest: use NameSpace.extern_flags with disabled "features" instead of internal NameSpace.get_accesses;
authorwenzelm
Tue Mar 03 14:54:12 2009 +0100 (2009-03-03)
changeset 302160300b7420b07
parent 30215 47cce3d47e62
child 30217 894eb2034f02
nicer_shortest: use NameSpace.extern_flags with disabled "features" instead of internal NameSpace.get_accesses;
src/Pure/Tools/find_theorems.ML
     1.1 --- a/src/Pure/Tools/find_theorems.ML	Tue Mar 03 14:53:29 2009 +0100
     1.2 +++ b/src/Pure/Tools/find_theorems.ML	Tue Mar 03 14:54:12 2009 +0100
     1.3 @@ -306,14 +306,11 @@
     1.4  
     1.5  fun nicer_shortest ctxt =
     1.6    let
     1.7 -    val ns = ProofContext.theory_of ctxt
     1.8 -             |> PureThy.facts_of
     1.9 -             |> Facts.space_of;
    1.10 +    (* FIXME global name space!? *)
    1.11 +    val space = Facts.space_of (PureThy.facts_of (ProofContext.theory_of ctxt));
    1.12  
    1.13 -    val len_sort = sort (int_ord o (pairself size));
    1.14 -    fun shorten s = (case len_sort (NameSpace.get_accesses ns s) of
    1.15 -                       [] => s
    1.16 -                     | s'::_ => s');
    1.17 +    val shorten =
    1.18 +      NameSpace.extern_flags {long_names = false, short_names = false, unique_names = false} space;
    1.19  
    1.20      fun nicer (Facts.Named ((x, _), i)) (Facts.Named ((y, _), j)) =
    1.21            nicer_name (shorten x, i) (shorten y, j)