# HG changeset patch
# User blanchet
# Date 1400759209 -7200
# Node ID be2602fbe58511cb2c32cb3c68b1b80f171775cd
# Parent  7a1167331c8cf482ceaec1c6e24cc5f8f052b533
properly mark relearns as dirty

diff -r 7a1167331c8c -r be2602fbe585 src/HOL/Tools/Sledgehammer/sledgehammer_mash.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_mash.ML	Thu May 22 13:07:53 2014 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_mash.ML	Thu May 22 13:46:49 2014 +0200
@@ -584,10 +584,10 @@
   Graph.default_node (parent, (Isar_Proof, [], []))
   #> Graph.add_edge (parent, name)
 
-fun add_node kind name parents feats deps =
-  Graph.default_node (name, (kind, feats, deps))
-  #> Graph.map_node name (K (kind, feats, deps))
-  #> fold (add_edge_to name) parents
+fun add_node kind name parents feats deps G =
+  (Graph.new_node (name, (kind, feats, deps)) G
+   handle Graph.DUP _ => Graph.map_node name (K (kind, feats, deps)) G)
+  |> fold (add_edge_to name) parents
 
 fun try_graph ctxt when def f =
   f ()
@@ -1391,7 +1391,7 @@
               val num_known_facts = num_known_facts + length learns
               val dirty =
                 (case (was_empty, dirty, relearns) of
-                  (false, SOME names, []) => SOME (map #1 learns @ names)
+                  (false, SOME names, []) => SOME (map #1 learns @ map #1 relearns @ names)
                 | _ => NONE)
             in
               if engine = MaSh_Py then