clarified order;
authorwenzelm
Thu, 11 Apr 2019 12:05:36 +0200
changeset 70301 3d580b5c4aee
parent 70299 c59af027a2e5
child 70302 5ae2f266885f
clarified order;
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