src/Pure/Tools/find_theorems.ML
changeset 42358 b47d41d9f4b5
parent 42012 2c3fe3cbebae
child 42360 da8817d01e7c
     1.1 --- a/src/Pure/Tools/find_theorems.ML	Sat Apr 16 12:46:18 2011 +0200
     1.2 +++ b/src/Pure/Tools/find_theorems.ML	Sat Apr 16 13:48:45 2011 +0200
     1.3 @@ -381,8 +381,11 @@
     1.4      val space = Facts.space_of (Global_Theory.facts_of (ProofContext.theory_of ctxt));
     1.5  
     1.6      val shorten =
     1.7 -      Name_Space.extern_flags
     1.8 -        {long_names = false, short_names = false, unique_names = false} space;
     1.9 +      Name_Space.extern
    1.10 +        (ctxt
    1.11 +          |> Config.put Name_Space.long_names false
    1.12 +          |> Config.put Name_Space.short_names false
    1.13 +          |> Config.put Name_Space.unique_names false) space;
    1.14  
    1.15      fun nicer (Facts.Named ((x, _), i)) (Facts.Named ((y, _), j)) =
    1.16            nicer_name (shorten x, i) (shorten y, j)