# HG changeset patch
# User blanchet
# Date 1342815585 -7200
# Node ID 4a11914fd53084fbb21c2e7cf951e101ad34f9f5
# Parent  416e4123baf36366bb4e5baeaf31ff48e2909568
fixed explosion when computing accessibility

diff -r 416e4123baf3 -r 4a11914fd530 src/HOL/Tools/Sledgehammer/sledgehammer_filter_mash.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_filter_mash.ML	Fri Jul 20 22:19:45 2012 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_filter_mash.ML	Fri Jul 20 22:19:45 2012 +0200
@@ -470,16 +470,17 @@
   let
     val facts = [] |> fold (cons o Thm.get_name_hint o snd) facts
     val tab = Symtab.empty |> fold (fn name => Symtab.update (name, ())) facts
-    fun insert_not_parent parents name =
-      not (member (op =) parents name) ? insert (op =) name
-    fun parents_of parents [] = parents
-      | parents_of parents (name :: names) =
+    fun insert_not_seen seen name =
+      not (member (op =) seen name) ? insert (op =) name
+    fun parents_of seen parents [] = parents
+      | parents_of seen parents (name :: names) =
         if Symtab.defined tab name then
-          parents_of (name :: parents) names
+          parents_of (name :: seen) (name :: parents) names
         else
-          parents_of parents (Graph.Keys.fold (insert_not_parent parents)
-                                  (Graph.imm_preds fact_graph name) names)
-  in parents_of [] (Graph.maximals fact_graph) end
+          parents_of (name :: seen) parents
+                     (Graph.Keys.fold (insert_not_seen seen)
+                                      (Graph.imm_preds fact_graph name) names)
+  in parents_of [] [] (Graph.maximals fact_graph) end
 
 (* Generate more suggestions than requested, because some might be thrown out
    later for various reasons and "meshing" gives better results with some