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 @@ -38,9 +38,6 @@
     1.4    val run_prover_for_mash :
     1.5      Proof.context -> params -> string -> fact list -> thm -> prover_result
     1.6    val mash_CLEAR : Proof.context -> unit
     1.7 -  val mash_INIT :
     1.8 -    Proof.context -> bool
     1.9 -    -> (string * string list * string list * string list) list -> unit
    1.10    val mash_ADD :
    1.11      Proof.context -> bool
    1.12      -> (string * string list * string list * string list) list -> unit
    1.13 @@ -341,22 +338,6 @@
    1.14      if not async then trace_msg ctxt (K "Done") else ()
    1.15    end
    1.16  
    1.17 -(* TODO: Eliminate code once "mash.py" handles sequences of ADD commands as fast
    1.18 -   as a single INIT. *)
    1.19 -fun run_mash_init ctxt overlord write_access write_feats write_deps =
    1.20 -  let
    1.21 -    val info as (temp_dir, serial) = mash_info overlord
    1.22 -    val in_dir = temp_dir ^ "/mash_init" ^ serial
    1.23 -                 |> tap (Path.explode #> Isabelle_System.mkdir)
    1.24 -  in
    1.25 -    write_file write_access (in_dir ^ "/mash_accessibility");
    1.26 -    write_file write_feats (in_dir ^ "/mash_features");
    1.27 -    write_file write_deps (in_dir ^ "/mash_dependencies");
    1.28 -    run_mash ctxt overlord info false
    1.29 -             ("--init --inputDir " ^ in_dir ^
    1.30 -              and_rm_files overlord " -r" [in_dir])
    1.31 -  end
    1.32 -
    1.33  fun run_mash_commands ctxt overlord save max_suggs write_cmds read_suggs =
    1.34    let
    1.35      val info as (temp_dir, serial) = mash_info overlord
    1.36 @@ -380,9 +361,6 @@
    1.37  fun str_of_query (parents, feats) =
    1.38    "? " ^ escape_metas parents ^ "; " ^ escape_metas feats
    1.39  
    1.40 -fun init_str_of_update get (upd as (name, _, _, _)) =
    1.41 -  escape_meta name ^ ": " ^ escape_metas (get upd) ^ "\n"
    1.42 -
    1.43  fun mash_CLEAR ctxt =
    1.44    let val path = mash_state_dir () |> Path.explode in
    1.45      trace_msg ctxt (K "MaSh CLEAR");
    1.46 @@ -391,13 +369,6 @@
    1.47                    path ()
    1.48    end
    1.49  
    1.50 -fun mash_INIT ctxt _ [] = mash_CLEAR ctxt
    1.51 -  | mash_INIT ctxt overlord upds =
    1.52 -    (trace_msg ctxt (fn () => "MaSh INIT " ^
    1.53 -         elide_string 1000 (space_implode " " (map #1 upds)));
    1.54 -     run_mash_init ctxt overlord (upds, init_str_of_update #2)
    1.55 -                   (upds, init_str_of_update #3) (upds, init_str_of_update #4))
    1.56 -
    1.57  fun mash_ADD _ _ [] = ()
    1.58    | mash_ADD ctxt overlord upds =
    1.59      (trace_msg ctxt (fn () => "MaSh ADD " ^
    1.60 @@ -627,12 +598,10 @@
    1.61          val n = length upds
    1.62          fun trans {thys, fact_graph} =
    1.63            let
    1.64 -            val mash_INIT_or_ADD =
    1.65 -              if Graph.is_empty fact_graph then mash_INIT else mash_ADD
    1.66              val (upds, fact_graph) =
    1.67                ([], fact_graph) |> fold (update_fact_graph ctxt) upds
    1.68            in
    1.69 -            (mash_INIT_or_ADD ctxt overlord (rev upds);
    1.70 +            (mash_ADD ctxt overlord (rev upds);
    1.71               {thys = thys |> add_thys_for thy, fact_graph = fact_graph})
    1.72            end
    1.73        in