1.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer_mash.ML	Mon Feb 18 08:52:23 2013 +0100
     1.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_mash.ML	Mon Feb 18 10:43:36 2013 +0100
     1.3 @@ -748,20 +748,19 @@
     1.4  
     1.5  fun num_keys keys = Graph.Keys.fold (K (Integer.add 1)) keys 0
     1.6  
     1.7 -fun maximal_in_graph access_G facts =
     1.8 +fun maximal_wrt_graph G keys =
     1.9    let
    1.10 -    val facts = [] |> fold (cons o nickname_of_thm o snd) facts
    1.11 -    val tab = Symtab.empty |> fold (fn name => Symtab.default (name, ())) facts
    1.12 +    val tab = Symtab.empty |> fold (fn name => Symtab.default (name, ())) keys
    1.13      fun insert_new seen name =
    1.14        not (Symtab.defined seen name) ? insert (op =) name
    1.15      fun find_maxes _ (maxs, []) = map snd maxs
    1.16        | find_maxes seen (maxs, new :: news) =
    1.17          find_maxes
    1.18 -            (seen |> num_keys (Graph.imm_succs access_G new) > 1
    1.19 +            (seen |> num_keys (Graph.imm_succs G new) > 1
    1.20                       ? Symtab.default (new, ()))
    1.21              (if Symtab.defined tab new then
    1.22                 let
    1.23 -                 val newp = Graph.all_preds access_G [new]
    1.24 +                 val newp = Graph.all_preds G [new]
    1.25                   fun is_ancestor x yp = member (op =) yp x
    1.26                   val maxs =
    1.27                     maxs |> filter (fn (_, max) => not (is_ancestor max newp))
    1.28 @@ -775,8 +774,12 @@
    1.29                 end
    1.30               else
    1.31                 (maxs, Graph.Keys.fold (insert_new seen)
    1.32 -                                      (Graph.imm_preds access_G new) news))
    1.33 -  in find_maxes Symtab.empty ([], Graph.maximals access_G) end
    1.34 +                                      (Graph.imm_preds G new) news))
    1.35 +  in find_maxes Symtab.empty ([], Graph.maximals G) end
    1.36 +
    1.37 +fun maximal_wrt_access_graph access_G =
    1.38 +  map (nickname_of_thm o snd)
    1.39 +  #> maximal_wrt_graph access_G
    1.40  
    1.41  fun is_fact_in_graph access_G get_th fact =
    1.42    can (Graph.get_node access_G) (nickname_of_thm (get_th fact))
    1.43 @@ -830,7 +833,7 @@
    1.44              (access_G, [])
    1.45            else
    1.46              let
    1.47 -              val parents = maximal_in_graph access_G facts
    1.48 +              val parents = maximal_wrt_access_graph access_G facts
    1.49                val feats =
    1.50                  features_of ctxt prover thy (Local, General) (concl_t :: hyp_ts)
    1.51                val hints =
    1.52 @@ -888,7 +891,7 @@
    1.53        in
    1.54          peek_state ctxt (fn {access_G, ...} =>
    1.55              let
    1.56 -              val parents = maximal_in_graph access_G facts
    1.57 +              val parents = maximal_wrt_access_graph access_G facts
    1.58                val deps =
    1.59                  used_ths |> filter (is_fact_in_graph access_G I)
    1.60                           |> map nickname_of_thm
    1.61 @@ -1003,7 +1006,7 @@
    1.62                val ancestors =
    1.63                  old_facts
    1.64                  |> filter (fn (_, th) => crude_thm_ord (th, last_th) <> GREATER)
    1.65 -              val parents = maximal_in_graph access_G ancestors
    1.66 +              val parents = maximal_wrt_access_graph access_G ancestors
    1.67                val (learns, (_, n, _, _)) =
    1.68                  ([], (parents, 0, next_commit_time (), false))
    1.69                  |> fold learn_new_fact new_facts