| changeset 59888 | 27e4d0ab0948 |
| parent 59498 | 50b60f501b05 |
| child 59916 | f673ce6b1e2b |
--- a/src/Pure/Tools/find_theorems.ML Tue Mar 31 23:42:57 2015 +0200 +++ b/src/Pure/Tools/find_theorems.ML Wed Apr 01 10:35:43 2015 +0200 @@ -328,7 +328,7 @@ local val index_ord = option_ord (K EQUAL); -val hidden_ord = bool_ord o apply2 Long_Name.is_hidden; +val hidden_ord = bool_ord o apply2 (is_some o Long_Name.dest_hidden); val qual_ord = int_ord o apply2 Long_Name.qualification; val txt_ord = int_ord o apply2 size;