1.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer_mash.ML	Thu Jul 24 18:46:38 2014 +0200
     1.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_mash.ML	Thu Jul 24 18:53:14 2014 +0200
     1.3 @@ -551,12 +551,15 @@
     1.4    Graph.default_node (parent, (Isar_Proof, [], []))
     1.5    #> Graph.add_edge (parent, name)
     1.6  
     1.7 -fun add_node kind name parents feats deps (access_G, (fact_xtab, feat_xtab), learns) =
     1.8 -  ((Graph.new_node (name, (kind, feats, deps)) access_G
     1.9 -    handle Graph.DUP _ => Graph.map_node name (K (kind, feats, deps)) access_G)
    1.10 -   |> fold (add_edge_to name) parents,
    1.11 -  (maybe_add_to_xtab name fact_xtab, fold maybe_add_to_xtab feats feat_xtab),
    1.12 -  (name, feats, deps) :: learns)
    1.13 +fun add_node kind name parents feats deps (accum as (access_G, (fact_xtab, feat_xtab), learns)) =
    1.14 +  let val fact_xtab' = add_to_xtab name fact_xtab in
    1.15 +    ((Graph.new_node (name, (kind, feats, deps)) access_G
    1.16 +      handle Graph.DUP _ => Graph.map_node name (K (kind, feats, deps)) access_G)
    1.17 +     |> fold (add_edge_to name) parents,
    1.18 +     (fact_xtab', fold maybe_add_to_xtab feats feat_xtab),
    1.19 +     (name, feats, deps) :: learns)
    1.20 +  end
    1.21 +  handle Symtab.DUP _ => accum (* robustness (in case the state file violates the invariant) *)
    1.22  
    1.23  fun try_graph ctxt when def f =
    1.24    f ()
    1.25 @@ -1211,7 +1214,8 @@
    1.26  
    1.27  fun mash_unlearn () = (clear_state (); Output.urgent_message "Reset MaSh.")
    1.28  
    1.29 -fun learn_wrt_access_graph ctxt (name, parents, feats, deps) (access_G, (fact_xtab, feat_xtab)) =
    1.30 +fun learn_wrt_access_graph ctxt (name, parents, feats, deps)
    1.31 +    (accum as (access_G, (fact_xtab, feat_xtab))) =
    1.32    let
    1.33      fun maybe_learn_from from (accum as (parents, access_G)) =
    1.34        try_graph ctxt "updating graph" accum (fn () =>
    1.35 @@ -1221,11 +1225,12 @@
    1.36      val (parents, access_G) = ([], access_G) |> fold maybe_learn_from parents
    1.37      val (deps, _) = ([], access_G) |> fold maybe_learn_from deps
    1.38  
    1.39 -    val fact_xtab = maybe_add_to_xtab name fact_xtab
    1.40 +    val fact_xtab = add_to_xtab name fact_xtab
    1.41      val feat_xtab = fold maybe_add_to_xtab feats feat_xtab
    1.42    in
    1.43 -    ((name, parents, feats, deps), (access_G, (fact_xtab, feat_xtab)))
    1.44 +    (SOME (name, parents, feats, deps), (access_G, (fact_xtab, feat_xtab)))
    1.45    end
    1.46 +  handle Symtab.DUP _ => (NONE, accum) (* facts sometimes have the same name, confusingly *)
    1.47  
    1.48  fun relearn_wrt_access_graph ctxt (name, deps) access_G =
    1.49    let
    1.50 @@ -1333,6 +1338,7 @@
    1.51  
    1.52                val (learns, (access_G', xtabs')) =
    1.53                  fold_map (learn_wrt_access_graph ctxt) learns (access_G, xtabs)
    1.54 +                |>> map_filter I
    1.55                val (relearns, access_G'') =
    1.56                  fold_map (relearn_wrt_access_graph ctxt) relearns access_G'
    1.57