1.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML	Tue Nov 19 15:45:45 2013 +0100
     1.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML	Tue Nov 19 16:48:50 2013 +0100
     1.3 @@ -838,9 +838,10 @@
     1.4                      Output.urgent_message "Generating proof text..."
     1.5                    else
     1.6                      ()
     1.7 +                val atp_proof = (fn () => termify_atp_proof ctxt pool lifted sym_tab atp_proof)
     1.8                  val isar_params =
     1.9 -                  (debug, verbose, preplay_timeout, isar_compress, isar_try0,
    1.10 -                   pool, fact_names, lifted, sym_tab, atp_proof, goal)
    1.11 +                  (debug, verbose, preplay_timeout, isar_compress, isar_try0, fact_names, atp_proof,
    1.12 +                   goal)
    1.13                  val one_line_params =
    1.14                    (preplay, proof_banner mode name, used_facts,
    1.15                     choose_minimize_command ctxt params minimize_command name

     2.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer_reconstruct.ML	Tue Nov 19 15:45:45 2013 +0100
     2.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_reconstruct.ML	Tue Nov 19 16:48:50 2013 +0100
     2.3 @@ -7,14 +7,14 @@
     2.4  
     2.5  signature SLEDGEHAMMER_RECONSTRUCT =
     2.6  sig
     2.7 +  type ('a, 'b) atp_step = ('a, 'b) ATP_Proof.atp_step
     2.8    type 'a atp_proof = 'a ATP_Proof.atp_proof
     2.9    type stature = ATP_Problem_Generate.stature
    2.10 -  type one_line_params = Sledgehammer_Print.one_line_params
    2.11 +  type one_line_params = Sledgehammer_Reconstructor.one_line_params
    2.12  
    2.13    type isar_params =
    2.14 -    bool * bool * Time.time option * real * bool * string Symtab.table
    2.15 -    * (string * stature) list vector * (string * term) list * int Symtab.table
    2.16 -    * string atp_proof * thm
    2.17 +    bool * bool * Time.time option * real * bool * (string * stature) list vector
    2.18 +    * (unit -> (term, string) atp_step list) * thm
    2.19  
    2.20    val lam_trans_of_atp_proof : string atp_proof -> string -> string
    2.21    val is_typed_helper_used_in_atp_proof : string atp_proof -> bool
    2.22 @@ -24,6 +24,9 @@
    2.23    val used_facts_in_unsound_atp_proof :
    2.24      Proof.context -> (string * stature) list vector -> 'a atp_proof ->
    2.25      string list option
    2.26 +  val termify_atp_proof :
    2.27 +    Proof.context -> string Symtab.table -> (string * term) list ->
    2.28 +    int Symtab.table -> string atp_proof -> (term, string) atp_step list
    2.29    val isar_proof_text :
    2.30      Proof.context -> bool option -> isar_params -> one_line_params -> string
    2.31    val proof_text :
    2.32 @@ -407,14 +410,19 @@
    2.33      and chain_proofs proofs = map (chain_proof) proofs
    2.34    in chain_proof end
    2.35  
    2.36 +fun termify_atp_proof ctxt pool lifted sym_tab =
    2.37 +  clean_up_atp_proof_dependencies
    2.38 +  #> nasty_atp_proof pool
    2.39 +  #> map_term_names_in_atp_proof repair_name
    2.40 +  #> map (decode_line ctxt lifted sym_tab)
    2.41 +  #> repair_waldmeister_endgame
    2.42 +
    2.43  type isar_params =
    2.44 -  bool * bool * Time.time option * real * bool * string Symtab.table
    2.45 -  * (string * stature) list vector * (string * term) list * int Symtab.table
    2.46 -  * string atp_proof * thm
    2.47 +  bool * bool * Time.time option * real * bool * (string * stature) list vector
    2.48 +  * (unit -> (term, string) atp_step list) * thm
    2.49  
    2.50  fun isar_proof_text ctxt isar_proofs
    2.51 -    (debug, verbose, preplay_timeout, isar_compress, isar_try0, pool,
    2.52 -     fact_names, lifted, sym_tab, atp_proof, goal)
    2.53 +    (debug, verbose, preplay_timeout, isar_compress, isar_try0, fact_names, atp_proof, goal)
    2.54      (one_line_params as (_, _, _, _, subgoal, subgoal_count)) =
    2.55    let
    2.56      val (params, hyp_ts, concl_t) = strip_subgoal goal subgoal ctxt
    2.57 @@ -425,6 +433,7 @@
    2.58               ctxt |> Variable.set_body false
    2.59                    |> Proof_Context.add_fixes fixes)
    2.60      val one_line_proof = one_line_proof_text 0 one_line_params
    2.61 +    val atp_proof = atp_proof ()
    2.62      val type_enc =
    2.63        if is_typed_helper_used_in_atp_proof atp_proof then full_typesN
    2.64        else partial_typesN
    2.65 @@ -435,11 +444,6 @@
    2.66        let
    2.67          val atp_proof =
    2.68            atp_proof
    2.69 -          |> clean_up_atp_proof_dependencies
    2.70 -          |> nasty_atp_proof pool
    2.71 -          |> map_term_names_in_atp_proof repair_name
    2.72 -          |> map (decode_line ctxt lifted sym_tab)
    2.73 -          |> repair_waldmeister_endgame
    2.74            |> rpair [] |-> fold_rev (add_line fact_names)
    2.75            |> rpair [] |-> fold_rev add_nontrivial_line
    2.76            |> rpair (0, [])

     3.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer_reconstructor.ML	Tue Nov 19 15:45:45 2013 +0100
     3.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_reconstructor.ML	Tue Nov 19 16:48:50 2013 +0100
     3.3 @@ -7,7 +7,6 @@
     3.4  
     3.5  signature SLEDGEHAMMER_RECONSTRUCTOR =
     3.6  sig
     3.7 -
     3.8    type stature = ATP_Problem_Generate.stature
     3.9  
    3.10    datatype reconstructor =
    3.11 @@ -25,8 +24,7 @@
    3.12      play * string * (string * stature) list * minimize_command * int * int
    3.13  
    3.14    val smtN : string
    3.15 -
    3.16 -end
    3.17 +end;
    3.18  
    3.19  structure Sledgehammer_Reconstructor : SLEDGEHAMMER_RECONSTRUCTOR =
    3.20  struct
    3.21 @@ -49,4 +47,4 @@
    3.22  
    3.23  val smtN = "smt"
    3.24  
    3.25 -end
    3.26 +end;