src/Pure/Tools/find_theorems.ML
changeset 42669 04dfffda5671
parent 42360 da8817d01e7c
child 43067 76e1d25c6357
     1.1 --- a/src/Pure/Tools/find_theorems.ML	Tue May 03 22:26:16 2011 +0200
     1.2 +++ b/src/Pure/Tools/find_theorems.ML	Tue May 03 22:27:32 2011 +0200
     1.3 @@ -383,9 +383,9 @@
     1.4      val shorten =
     1.5        Name_Space.extern
     1.6          (ctxt
     1.7 -          |> Config.put Name_Space.long_names false
     1.8 -          |> Config.put Name_Space.short_names false
     1.9 -          |> Config.put Name_Space.unique_names false) space;
    1.10 +          |> Config.put Name_Space.names_long false
    1.11 +          |> Config.put Name_Space.names_short false
    1.12 +          |> Config.put Name_Space.names_unique false) space;
    1.13  
    1.14      fun nicer (Facts.Named ((x, _), i)) (Facts.Named ((y, _), j)) =
    1.15            nicer_name (shorten x, i) (shorten y, j)