# HG changeset patch
# User blanchet
# Date 1471170369 -7200
# Node ID 4de35d16e53377e55441c7bb41f22b374a0d8be0
# Parent  0afe49623cf921ce8fed14ecdedf857b9406fe02
optimized parent computation in MaSh

diff -r 0afe49623cf9 -r 4de35d16e533 src/HOL/Tools/Sledgehammer/sledgehammer_mash.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_mash.ML	Sun Aug 14 12:26:09 2016 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_mash.ML	Sun Aug 14 12:26:09 2016 +0200
@@ -1156,11 +1156,29 @@
           G |> Graph.restrict (not o String.isPrefix anonymous_proof_prefix) |> Graph.maximals)
       end
 
+val max_facts_for_shuffle_cleanup = 20
+
 fun maximal_wrt_access_graph _ [] = []
-  | maximal_wrt_access_graph access_G ((fact as (_, th)) :: facts) =
-    let val thy_id = Thm.theory_id_of_thm th in
-      fact :: filter_out (fn (_, th') =>
-        Context.proper_subthy_id (Thm.theory_id_of_thm th', thy_id)) facts
+  | maximal_wrt_access_graph access_G (fact :: facts) =
+    let
+      fun cleanup_wrt (fact as (_, th)) =
+        let val thy_id = Thm.theory_id_of_thm th in
+          filter_out (fn (_, th') =>
+            Context.proper_subthy_id (Thm.theory_id_of_thm th', thy_id))
+        end
+
+      fun shuffle_cleanup accum [] = accum
+        | shuffle_cleanup accum (fact :: facts) =
+          let
+            val accum' = accum |> cleanup_wrt fact
+            val facts' = facts |> cleanup_wrt fact
+          in
+            shuffle_cleanup accum' facts'
+          end
+    in
+      fact :: cleanup_wrt fact facts
+      |> (fn facts => facts
+        |> length facts <= max_facts_for_shuffle_cleanup ? shuffle_cleanup [])
       |> map (nickname_of_thm o snd)
       |> maximal_wrt_graph access_G
     end