# HG changeset patch
# User blanchet
# Date 1406220794 -7200
# Node ID 1586d0479f2c6937cd7a7c4671e9b81c3ecf3dca
# Parent  86b853448f08df6a11591d6c7621c7a136fc6048
eliminated source of 'DUP's in MaSh

diff -r 86b853448f08 -r 1586d0479f2c src/HOL/Tools/Sledgehammer/sledgehammer_mash.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_mash.ML	Thu Jul 24 18:46:38 2014 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_mash.ML	Thu Jul 24 18:53:14 2014 +0200
@@ -551,12 +551,15 @@
   Graph.default_node (parent, (Isar_Proof, [], []))
   #> Graph.add_edge (parent, name)
 
-fun add_node kind name parents feats deps (access_G, (fact_xtab, feat_xtab), learns) =
-  ((Graph.new_node (name, (kind, feats, deps)) access_G
-    handle Graph.DUP _ => Graph.map_node name (K (kind, feats, deps)) access_G)
-   |> fold (add_edge_to name) parents,
-  (maybe_add_to_xtab name fact_xtab, fold maybe_add_to_xtab feats feat_xtab),
-  (name, feats, deps) :: learns)
+fun add_node kind name parents feats deps (accum as (access_G, (fact_xtab, feat_xtab), learns)) =
+  let val fact_xtab' = add_to_xtab name fact_xtab in
+    ((Graph.new_node (name, (kind, feats, deps)) access_G
+      handle Graph.DUP _ => Graph.map_node name (K (kind, feats, deps)) access_G)
+     |> fold (add_edge_to name) parents,
+     (fact_xtab', fold maybe_add_to_xtab feats feat_xtab),
+     (name, feats, deps) :: learns)
+  end
+  handle Symtab.DUP _ => accum (* robustness (in case the state file violates the invariant) *)
 
 fun try_graph ctxt when def f =
   f ()
@@ -1211,7 +1214,8 @@
 
 fun mash_unlearn () = (clear_state (); Output.urgent_message "Reset MaSh.")
 
-fun learn_wrt_access_graph ctxt (name, parents, feats, deps) (access_G, (fact_xtab, feat_xtab)) =
+fun learn_wrt_access_graph ctxt (name, parents, feats, deps)
+    (accum as (access_G, (fact_xtab, feat_xtab))) =
   let
     fun maybe_learn_from from (accum as (parents, access_G)) =
       try_graph ctxt "updating graph" accum (fn () =>
@@ -1221,11 +1225,12 @@
     val (parents, access_G) = ([], access_G) |> fold maybe_learn_from parents
     val (deps, _) = ([], access_G) |> fold maybe_learn_from deps
 
-    val fact_xtab = maybe_add_to_xtab name fact_xtab
+    val fact_xtab = add_to_xtab name fact_xtab
     val feat_xtab = fold maybe_add_to_xtab feats feat_xtab
   in
-    ((name, parents, feats, deps), (access_G, (fact_xtab, feat_xtab)))
+    (SOME (name, parents, feats, deps), (access_G, (fact_xtab, feat_xtab)))
   end
+  handle Symtab.DUP _ => (NONE, accum) (* facts sometimes have the same name, confusingly *)
 
 fun relearn_wrt_access_graph ctxt (name, deps) access_G =
   let
@@ -1333,6 +1338,7 @@
 
               val (learns, (access_G', xtabs')) =
                 fold_map (learn_wrt_access_graph ctxt) learns (access_G, xtabs)
+                |>> map_filter I
               val (relearns, access_G'') =
                 fold_map (relearn_wrt_access_graph ctxt) relearns access_G'