--- a/src/HOL/Tools/Quickcheck/find_unused_assms.ML Wed Apr 10 23:12:27 2019 +0100
+++ b/src/HOL/Tools/Quickcheck/find_unused_assms.ML Thu Apr 11 12:05:36 2019 +0200
@@ -40,8 +40,9 @@
|> Config.put Quickcheck.abort_potential true
|> Config.put Quickcheck.quiet true
val all_thms =
- filter (fn (s, _) => length (Long_Name.explode s) = 2) (* FIXME !? *)
- (thms_of thy thy_name)
+ thms_of thy thy_name
+ |> filter (fn (s, _) => length (Long_Name.explode s) = 2) (* FIXME !? *)
+ |> sort_by #1
fun check_single conjecture =
(case try (Quickcheck.test_terms ctxt' (true, true) []) [(conjecture, [])] of
SOME (SOME _) => false