1.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer_mash.ML	Fri Jul 20 22:19:46 2012 +0200
     1.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_mash.ML	Fri Jul 20 22:19:46 2012 +0200
     1.3 @@ -613,24 +613,17 @@
     1.4    if is_smt_prover ctxt prover then
     1.5      ()
     1.6    else
     1.7 -    launch_thread timeout
     1.8 -        (fn () =>
     1.9 -            let
    1.10 -              val thy = Proof_Context.theory_of ctxt
    1.11 -              val name = freshish_name ()
    1.12 -              val feats = features_of ctxt prover thy (Local, General) [t]
    1.13 -              val deps = used_ths |> map nickname_of
    1.14 -            in
    1.15 -              mash_map ctxt (fn {fact_G} =>
    1.16 -                  let
    1.17 -                    val parents = max_facts_in_graph fact_G facts
    1.18 -                    val upds = [(name, parents, feats, deps)]
    1.19 -                    val (upds, fact_G) =
    1.20 -                      ([], fact_G) |> fold (update_fact_graph ctxt) upds
    1.21 -                  in mash_ADD ctxt overlord upds; {fact_G = fact_G}
    1.22 -                  end);
    1.23 -              (true, "")
    1.24 -            end)
    1.25 +    launch_thread timeout (fn () =>
    1.26 +        let
    1.27 +          val thy = Proof_Context.theory_of ctxt
    1.28 +          val name = freshish_name ()
    1.29 +          val feats = features_of ctxt prover thy (Local, General) [t]
    1.30 +          val deps = used_ths |> map nickname_of
    1.31 +          val {fact_G} = mash_get ctxt
    1.32 +          val parents = max_facts_in_graph fact_G facts
    1.33 +        in
    1.34 +          mash_ADD ctxt overlord [(name, parents, feats, deps)]; (true, "")
    1.35 +        end)
    1.36  
    1.37  fun sendback sub =
    1.38    Markup.markup Isabelle_Markup.sendback (sledgehammerN ^ " " ^ sub)