src/HOL/Tools/Sledgehammer/sledgehammer_prover.ML
changeset 55202 824c48a539c9
parent 55201 1ee776da8da7
child 55205 8450622db0c5
     1.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer_prover.ML	Fri Jan 31 10:23:32 2014 +0100
     1.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_prover.ML	Fri Jan 31 10:23:32 2014 +0100
     1.3 @@ -127,8 +127,8 @@
     1.4  open Sledgehammer_Util
     1.5  open Sledgehammer_Fact
     1.6  open Sledgehammer_Reconstructor
     1.7 -open Sledgehammer_Print
     1.8 -open Sledgehammer_Reconstruct
     1.9 +open Sledgehammer_Isar_Print
    1.10 +open Sledgehammer_Isar
    1.11  
    1.12  
    1.13  (** The Sledgehammer **)
    1.14 @@ -503,8 +503,8 @@
    1.15      else remotify_prover_if_not_installed ctxt eN |> the_default name
    1.16    end
    1.17  
    1.18 -(* See the analogous logic in the function "maybe_minimize" in
    1.19 -  "sledgehammer_minimize.ML". *)
    1.20 +(* FIXME: See the analogous logic in the function "maybe_minimize" in
    1.21 +   "sledgehammer_prover_minimize.ML". *)
    1.22  fun choose_minimize_command ctxt (params as {isar_proofs, ...}) minimize_command name preplay =
    1.23    let
    1.24      val maybe_isar_name = name |> isar_proofs = SOME true ? isar_proof_reconstructor ctxt