1.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer_mash.ML	Mon Jul 23 15:32:30 2012 +0200
     1.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_mash.ML	Mon Jul 23 15:32:30 2012 +0200
     1.3 @@ -551,6 +551,9 @@
     1.4  fun mash_map ctxt f =
     1.5    Synchronized.change global_state (load ctxt ##> (f #> tap (save ctxt)))
     1.6  
     1.7 +fun mash_peek ctxt f =
     1.8 +  Synchronized.change_result global_state (load ctxt #> `snd #>> f)
     1.9 +
    1.10  fun mash_get ctxt =
    1.11    Synchronized.change_result global_state (load ctxt #> `snd)
    1.12  
    1.13 @@ -598,7 +601,7 @@
    1.14  (* Generate more suggestions than requested, because some might be thrown out
    1.15     later for various reasons and "meshing" gives better results with some
    1.16     slack. *)
    1.17 -fun max_suggs_of max_facts = max_facts + Int.min (200, max_facts)
    1.18 +fun max_suggs_of max_facts = max_facts + Int.min (50, max_facts)
    1.19  
    1.20  fun is_fact_in_graph fact_G (_, th) =
    1.21    can (Graph.get_node fact_G) (nickname_of th)
    1.22 @@ -607,12 +610,19 @@
    1.23                           concl_t facts =
    1.24    let
    1.25      val thy = Proof_Context.theory_of ctxt
    1.26 -    val fact_G = #fact_G (mash_get ctxt)
    1.27 -    val parents = maximal_in_graph fact_G facts
    1.28 -    val feats = features_of ctxt prover thy (Local, General) (concl_t :: hyp_ts)
    1.29 -    val suggs =
    1.30 -      if Graph.is_empty fact_G then []
    1.31 -      else mash_QUERY ctxt overlord (max_suggs_of max_facts) (parents, feats)
    1.32 +    val (fact_G, suggs) =
    1.33 +      mash_peek ctxt (fn {fact_G} =>
    1.34 +          if Graph.is_empty fact_G then
    1.35 +            (fact_G, [])
    1.36 +          else
    1.37 +            let
    1.38 +              val parents = maximal_in_graph fact_G facts
    1.39 +              val feats =
    1.40 +                features_of ctxt prover thy (Local, General) (concl_t :: hyp_ts)
    1.41 +            in
    1.42 +              (fact_G, mash_QUERY ctxt overlord (max_suggs_of max_facts)
    1.43 +                                  (parents, feats))
    1.44 +            end)
    1.45      val selected =
    1.46        facts |> suggested_facts suggs
    1.47              (* The weights currently returned by "mash.py" are too extreme to
    1.48 @@ -656,10 +666,12 @@
    1.49            val name = freshish_name ()
    1.50            val feats = features_of ctxt prover thy (Local, General) [t]
    1.51            val deps = used_ths |> map nickname_of
    1.52 -          val {fact_G} = mash_get ctxt
    1.53 -          val parents = maximal_in_graph fact_G facts
    1.54          in
    1.55 -          mash_ADD ctxt overlord [(name, parents, feats, deps)]; (true, "")
    1.56 +          mash_peek ctxt (fn {fact_G} =>
    1.57 +              let val parents = maximal_in_graph fact_G facts in
    1.58 +                mash_ADD ctxt overlord [(name, parents, feats, deps)]
    1.59 +              end);
    1.60 +          (true, "")
    1.61          end)
    1.62  
    1.63  fun sendback sub =