1.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer_mash.ML	Fri Jul 20 22:19:46 2012 +0200
     1.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_mash.ML	Fri Jul 20 22:19:46 2012 +0200
     1.3 @@ -546,19 +546,20 @@
     1.4      fun enqueue_new seen name =
     1.5        not (member (op =) seen name) ? Queue.enqueue name
     1.6      fun find_maxes seen maxs names =
     1.7 -        case try Queue.dequeue names of
     1.8 -          NONE => maxs
     1.9 -        | SOME (name, names) =>
    1.10 -          if Symtab.defined tab name then
    1.11 -            let
    1.12 -              fun no_path x y = not (member (op =) (Graph.all_preds fact_G [y]) x)
    1.13 -              val maxs = maxs |> filter (fn max => no_path max name)
    1.14 -              val maxs = maxs |> forall (no_path name) maxs ? cons name
    1.15 -            in find_maxes (name :: seen) maxs names end
    1.16 -          else
    1.17 -            find_maxes (name :: seen) maxs
    1.18 -                       (Graph.Keys.fold (enqueue_new seen)
    1.19 -                                        (Graph.imm_preds fact_G name) names)
    1.20 +      case try Queue.dequeue names of
    1.21 +        NONE => map snd maxs
    1.22 +      | SOME (name, names) =>
    1.23 +        if Symtab.defined tab name then
    1.24 +          let
    1.25 +            val new = (Graph.all_preds fact_G [name], name)
    1.26 +            fun not_ancestor (_, x) (yp, _) = not (member (op =) yp x)
    1.27 +            val maxs = maxs |> filter (fn max => not_ancestor max new)
    1.28 +            val maxs = maxs |> forall (not_ancestor new) maxs ? cons new
    1.29 +          in find_maxes (name :: seen) maxs names end
    1.30 +        else
    1.31 +          find_maxes (name :: seen) maxs
    1.32 +                     (Graph.Keys.fold (enqueue_new seen)
    1.33 +                                      (Graph.imm_preds fact_G name) names)
    1.34    in find_maxes [] [] (queue_of (Graph.maximals fact_G)) end
    1.35  
    1.36  (* Generate more suggestions than requested, because some might be thrown out