equal
deleted
inserted
replaced
953 old_facts @ facts |
953 old_facts @ facts |
954 |> do_facts (chunks_and_parents_for [[]] th) |
954 |> do_facts (chunks_and_parents_for [[]] th) |
955 |> drop (length old_facts) |
955 |> drop (length old_facts) |
956 end |
956 end |
957 |
957 |
958 fun sendback sub = Active.sendback_markup (sledgehammerN ^ " " ^ sub) |
958 fun sendback sub = |
|
959 Active.sendback_markup [Markup.padding_command] (sledgehammerN ^ " " ^ sub) |
959 |
960 |
960 val commit_timeout = seconds 30.0 |
961 val commit_timeout = seconds 30.0 |
961 |
962 |
962 (* The timeout is understood in a very relaxed fashion. *) |
963 (* The timeout is understood in a very relaxed fashion. *) |
963 fun mash_learn_facts ctxt (params as {debug, verbose, overlord, ...}) prover |
964 fun mash_learn_facts ctxt (params as {debug, verbose, overlord, ...}) prover |