# HG changeset patch
# User blanchet
# Date 1342815586 -7200
# Node ID e740216ca28df088141927196bd5f6086389629a
# Parent  f08425165cca31a5782c19f912729eca56cfa57c
cached ancestor computation

diff -r f08425165cca -r e740216ca28d src/HOL/Tools/Sledgehammer/sledgehammer_mash.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_mash.ML	Fri Jul 20 22:19:46 2012 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_mash.ML	Fri Jul 20 22:19:46 2012 +0200
@@ -546,19 +546,20 @@
     fun enqueue_new seen name =
       not (member (op =) seen name) ? Queue.enqueue name
     fun find_maxes seen maxs names =
-        case try Queue.dequeue names of
-          NONE => maxs
-        | SOME (name, names) =>
-          if Symtab.defined tab name then
-            let
-              fun no_path x y = not (member (op =) (Graph.all_preds fact_G [y]) x)
-              val maxs = maxs |> filter (fn max => no_path max name)
-              val maxs = maxs |> forall (no_path name) maxs ? cons name
-            in find_maxes (name :: seen) maxs names end
-          else
-            find_maxes (name :: seen) maxs
-                       (Graph.Keys.fold (enqueue_new seen)
-                                        (Graph.imm_preds fact_G name) names)
+      case try Queue.dequeue names of
+        NONE => map snd maxs
+      | SOME (name, names) =>
+        if Symtab.defined tab name then
+          let
+            val new = (Graph.all_preds fact_G [name], name)
+            fun not_ancestor (_, x) (yp, _) = not (member (op =) yp x)
+            val maxs = maxs |> filter (fn max => not_ancestor max new)
+            val maxs = maxs |> forall (not_ancestor new) maxs ? cons new
+          in find_maxes (name :: seen) maxs names end
+        else
+          find_maxes (name :: seen) maxs
+                     (Graph.Keys.fold (enqueue_new seen)
+                                      (Graph.imm_preds fact_G name) names)
   in find_maxes [] [] (queue_of (Graph.maximals fact_G)) end
 
 (* Generate more suggestions than requested, because some might be thrown out