1.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer_filter_mash.ML	Fri Jul 20 22:19:45 2012 +0200
     1.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_filter_mash.ML	Fri Jul 20 22:19:45 2012 +0200
     1.3 @@ -470,16 +470,17 @@
     1.4    let
     1.5      val facts = [] |> fold (cons o Thm.get_name_hint o snd) facts
     1.6      val tab = Symtab.empty |> fold (fn name => Symtab.update (name, ())) facts
     1.7 -    fun insert_not_parent parents name =
     1.8 -      not (member (op =) parents name) ? insert (op =) name
     1.9 -    fun parents_of parents [] = parents
    1.10 -      | parents_of parents (name :: names) =
    1.11 +    fun insert_not_seen seen name =
    1.12 +      not (member (op =) seen name) ? insert (op =) name
    1.13 +    fun parents_of seen parents [] = parents
    1.14 +      | parents_of seen parents (name :: names) =
    1.15          if Symtab.defined tab name then
    1.16 -          parents_of (name :: parents) names
    1.17 +          parents_of (name :: seen) (name :: parents) names
    1.18          else
    1.19 -          parents_of parents (Graph.Keys.fold (insert_not_parent parents)
    1.20 -                                  (Graph.imm_preds fact_graph name) names)
    1.21 -  in parents_of [] (Graph.maximals fact_graph) end
    1.22 +          parents_of (name :: seen) parents
    1.23 +                     (Graph.Keys.fold (insert_not_seen seen)
    1.24 +                                      (Graph.imm_preds fact_graph name) names)
    1.25 +  in parents_of [] [] (Graph.maximals fact_graph) end
    1.26  
    1.27  (* Generate more suggestions than requested, because some might be thrown out
    1.28     later for various reasons and "meshing" gives better results with some