# HG changeset patch
# User blanchet
# Date 1361180616 -3600
# Node ID 407b0258464b597842dd17fd52ef9a7ed4545007
# Parent  9f472d5f112c89c571ab21f8d7e7f066762070bd
tuned code

diff -r 9f472d5f112c -r 407b0258464b src/HOL/Tools/Sledgehammer/sledgehammer_mash.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_mash.ML	Mon Feb 18 08:52:23 2013 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_mash.ML	Mon Feb 18 10:43:36 2013 +0100
@@ -748,20 +748,19 @@
 
 fun num_keys keys = Graph.Keys.fold (K (Integer.add 1)) keys 0
 
-fun maximal_in_graph access_G facts =
+fun maximal_wrt_graph G keys =
   let
-    val facts = [] |> fold (cons o nickname_of_thm o snd) facts
-    val tab = Symtab.empty |> fold (fn name => Symtab.default (name, ())) facts
+    val tab = Symtab.empty |> fold (fn name => Symtab.default (name, ())) keys
     fun insert_new seen name =
       not (Symtab.defined seen name) ? insert (op =) name
     fun find_maxes _ (maxs, []) = map snd maxs
       | find_maxes seen (maxs, new :: news) =
         find_maxes
-            (seen |> num_keys (Graph.imm_succs access_G new) > 1
+            (seen |> num_keys (Graph.imm_succs G new) > 1
                      ? Symtab.default (new, ()))
             (if Symtab.defined tab new then
                let
-                 val newp = Graph.all_preds access_G [new]
+                 val newp = Graph.all_preds G [new]
                  fun is_ancestor x yp = member (op =) yp x
                  val maxs =
                    maxs |> filter (fn (_, max) => not (is_ancestor max newp))
@@ -775,8 +774,12 @@
                end
              else
                (maxs, Graph.Keys.fold (insert_new seen)
-                                      (Graph.imm_preds access_G new) news))
-  in find_maxes Symtab.empty ([], Graph.maximals access_G) end
+                                      (Graph.imm_preds G new) news))
+  in find_maxes Symtab.empty ([], Graph.maximals G) end
+
+fun maximal_wrt_access_graph access_G =
+  map (nickname_of_thm o snd)
+  #> maximal_wrt_graph access_G
 
 fun is_fact_in_graph access_G get_th fact =
   can (Graph.get_node access_G) (nickname_of_thm (get_th fact))
@@ -830,7 +833,7 @@
             (access_G, [])
           else
             let
-              val parents = maximal_in_graph access_G facts
+              val parents = maximal_wrt_access_graph access_G facts
               val feats =
                 features_of ctxt prover thy (Local, General) (concl_t :: hyp_ts)
               val hints =
@@ -888,7 +891,7 @@
       in
         peek_state ctxt (fn {access_G, ...} =>
             let
-              val parents = maximal_in_graph access_G facts
+              val parents = maximal_wrt_access_graph access_G facts
               val deps =
                 used_ths |> filter (is_fact_in_graph access_G I)
                          |> map nickname_of_thm
@@ -1003,7 +1006,7 @@
               val ancestors =
                 old_facts
                 |> filter (fn (_, th) => crude_thm_ord (th, last_th) <> GREATER)
-              val parents = maximal_in_graph access_G ancestors
+              val parents = maximal_wrt_access_graph access_G ancestors
               val (learns, (_, n, _, _)) =
                 ([], (parents, 0, next_commit_time (), false))
                 |> fold learn_new_fact new_facts