# HG changeset patch
# User blanchet
# Date 1380632532 -7200
# Node ID 7a8263843acb6dbf2dfe12a9302238456eacaa84
# Parent  427b7723874677f5fbfe28734ca2f78f650b09cf
removed spurious save if nothing needs to bee learned

diff -r 427b77238746 -r 7a8263843acb src/HOL/Tools/Sledgehammer/sledgehammer_mash.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_mash.ML	Tue Oct 01 14:40:25 2013 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_mash.ML	Tue Oct 01 15:02:12 2013 +0200
@@ -1320,12 +1320,17 @@
             val {access_G, num_known_facts, ...} = peek_state ctxt overlord I
             val is_in_access_G = is_fact_in_graph access_G o snd
           in
-            if length facts - num_known_facts <= max_facts_to_learn_before_query
-               andalso length (filter_out is_in_access_G facts)
-                       <= max_facts_to_learn_before_query then
-              (mash_learn_facts ctxt params prover false 2 false timeout facts
-               |> (fn "" => () | s => Output.urgent_message (MaShN ^ ": " ^ s));
-               true)
+            if length facts - num_known_facts
+               <= max_facts_to_learn_before_query then
+              case length (filter_out is_in_access_G facts) of
+                0 => false
+              | num_facts_to_learn =>
+                if num_facts_to_learn <= max_facts_to_learn_before_query then
+                  (mash_learn_facts ctxt params prover false 2 false timeout facts
+                   |> (fn "" => () | s => Output.urgent_message (MaShN ^ ": " ^ s));
+                   true)
+                else
+                  (maybe_launch_thread (); false)
             else
               (maybe_launch_thread (); false)
           end