# HG changeset patch
# User wenzelm
# Date 1554977136 -7200
# Node ID 3d580b5c4aee61711131045f366e82382a816dba
# Parent  c59af027a2e5041da725a0f5b816422382f64592
clarified order;

diff -r c59af027a2e5 -r 3d580b5c4aee src/HOL/Tools/Quickcheck/find_unused_assms.ML
--- 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