src/Pure/Tools/find_theorems.ML
changeset 59916 f673ce6b1e2b
parent 59888 27e4d0ab0948
child 59934 b65c4370f831
equal deleted inserted replaced
59915:7d5b2f4c621c 59916:f673ce6b1e2b
   326 (* removing duplicates, preferring nicer names, roughly O(n log n) *)
   326 (* removing duplicates, preferring nicer names, roughly O(n log n) *)
   327 
   327 
   328 local
   328 local
   329 
   329 
   330 val index_ord = option_ord (K EQUAL);
   330 val index_ord = option_ord (K EQUAL);
   331 val hidden_ord = bool_ord o apply2 (is_some o Long_Name.dest_hidden);
   331 val hidden_ord = bool_ord o apply2 Long_Name.is_hidden;
   332 val qual_ord = int_ord o apply2 Long_Name.qualification;
   332 val qual_ord = int_ord o apply2 Long_Name.qualification;
   333 val txt_ord = int_ord o apply2 size;
   333 val txt_ord = int_ord o apply2 size;
   334 
   334 
   335 fun nicer_name (x, i) (y, j) =
   335 fun nicer_name (x, i) (y, j) =
   336   (case hidden_ord (x, y) of EQUAL =>
   336   (case hidden_ord (x, y) of EQUAL =>