# HG changeset patch
# User blanchet
# Date 1342815586 -7200
# Node ID 1f214c653c80ed0d88e788684e5fee11bda868ae
# Parent  327ebf1c42a8a4ace7daab841eabed0d261aacd1
don't store fresh names in fact graph, since these cannot be the parents of any other facts

diff -r 327ebf1c42a8 -r 1f214c653c80 src/HOL/Tools/Sledgehammer/sledgehammer_mash.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_mash.ML	Fri Jul 20 22:19:46 2012 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_mash.ML	Fri Jul 20 22:19:46 2012 +0200
@@ -613,24 +613,17 @@
   if is_smt_prover ctxt prover then
     ()
   else
-    launch_thread timeout
-        (fn () =>
-            let
-              val thy = Proof_Context.theory_of ctxt
-              val name = freshish_name ()
-              val feats = features_of ctxt prover thy (Local, General) [t]
-              val deps = used_ths |> map nickname_of
-            in
-              mash_map ctxt (fn {fact_G} =>
-                  let
-                    val parents = max_facts_in_graph fact_G facts
-                    val upds = [(name, parents, feats, deps)]
-                    val (upds, fact_G) =
-                      ([], fact_G) |> fold (update_fact_graph ctxt) upds
-                  in mash_ADD ctxt overlord upds; {fact_G = fact_G}
-                  end);
-              (true, "")
-            end)
+    launch_thread timeout (fn () =>
+        let
+          val thy = Proof_Context.theory_of ctxt
+          val name = freshish_name ()
+          val feats = features_of ctxt prover thy (Local, General) [t]
+          val deps = used_ths |> map nickname_of
+          val {fact_G} = mash_get ctxt
+          val parents = max_facts_in_graph fact_G facts
+        in
+          mash_ADD ctxt overlord [(name, parents, feats, deps)]; (true, "")
+        end)
 
 fun sendback sub =
   Markup.markup Isabelle_Markup.sendback (sledgehammerN ^ " " ^ sub)