1.1 --- a/src/HOL/Mirabelle/Tools/mirabelle_sledgehammer.ML	Mon Jan 23 17:40:31 2012 +0100
     1.2 +++ b/src/HOL/Mirabelle/Tools/mirabelle_sledgehammer.ML	Mon Jan 23 17:40:32 2012 +0100
     1.3 @@ -336,7 +336,7 @@
     1.4      | NONE => get_prover (default_prover_name ()))
     1.5    end
     1.6  
     1.7 -type locality = ATP_Translate.locality
     1.8 +type locality = ATP_Problem_Generate.locality
     1.9  
    1.10  (* hack *)
    1.11  fun reconstructor_from_msg args msg =
    1.12 @@ -410,7 +410,7 @@
    1.13      fun failed failure =
    1.14        ({outcome = SOME failure, used_facts = [], run_time = Time.zeroTime,
    1.15          preplay =
    1.16 -          K (ATP_Reconstruct.Failed_to_Play Sledgehammer_Provers.plain_metis),
    1.17 +          K (ATP_Proof_Reconstruct.Failed_to_Play Sledgehammer_Provers.plain_metis),
    1.18          message = K "", message_tail = ""}, ~1)
    1.19      val ({outcome, used_facts, run_time, preplay, message, message_tail}
    1.20           : Sledgehammer_Provers.prover_result,
    1.21 @@ -581,12 +581,13 @@
    1.22            ORELSE' sledge_tac 0.2 ATP_Systems.eN "mono_guards??"
    1.23            ORELSE' sledge_tac 0.2 ATP_Systems.vampireN "mono_guards??"
    1.24            ORELSE' sledge_tac 0.2 ATP_Systems.spassN "poly_tags"
    1.25 -          ORELSE' Metis_Tactic.metis_tac [] ATP_Translate.combinatorsN ctxt thms
    1.26 +          ORELSE' Metis_Tactic.metis_tac [] ATP_Problem_Generate.combinatorsN
    1.27 +            ctxt thms
    1.28          else if !reconstructor = "smt" then
    1.29            SMT_Solver.smt_tac ctxt thms
    1.30          else if full then
    1.31 -          Metis_Tactic.metis_tac [ATP_Reconstruct.full_typesN]
    1.32 -            ATP_Reconstruct.metis_default_lam_trans ctxt thms
    1.33 +          Metis_Tactic.metis_tac [ATP_Proof_Reconstruct.full_typesN]
    1.34 +            ATP_Proof_Reconstruct.metis_default_lam_trans ctxt thms
    1.35          else if String.isPrefix "metis (" (!reconstructor) then
    1.36            let
    1.37              val (type_encs, lam_trans) =
    1.38 @@ -594,11 +595,11 @@
    1.39                |> Outer_Syntax.scan Position.start
    1.40                |> filter Token.is_proper |> tl
    1.41                |> Metis_Tactic.parse_metis_options |> fst
    1.42 -              |>> the_default [ATP_Reconstruct.partial_typesN]
    1.43 -              ||> the_default ATP_Reconstruct.metis_default_lam_trans
    1.44 +              |>> the_default [ATP_Proof_Reconstruct.partial_typesN]
    1.45 +              ||> the_default ATP_Proof_Reconstruct.metis_default_lam_trans
    1.46            in Metis_Tactic.metis_tac type_encs lam_trans ctxt thms end
    1.47          else if !reconstructor = "metis" then
    1.48 -          Metis_Tactic.metis_tac [] ATP_Reconstruct.metis_default_lam_trans ctxt
    1.49 +          Metis_Tactic.metis_tac [] ATP_Proof_Reconstruct.metis_default_lam_trans ctxt
    1.50              thms
    1.51          else
    1.52            K all_tac