src/HOL/Tools/Sledgehammer/sledgehammer_prover.ML
changeset 56985 82c83978fbd9
parent 56983 132142089ea6
child 57037 c51132be8e16
     1.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer_prover.ML	Fri May 16 19:13:50 2014 +0200
     1.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_prover.ML	Fri May 16 19:14:00 2014 +0200
     1.3 @@ -216,6 +216,8 @@
     1.4  
     1.5  fun play_one_line_proof mode debug verbose timeout pairs state i preferred (meths as meth :: _) =
     1.6    let
     1.7 +    val ctxt = Proof.context_of state
     1.8 +
     1.9      fun get_preferred meths = if member (op =) meths preferred then preferred else meth
    1.10    in
    1.11      if timeout = Time.zeroTime then
    1.12 @@ -230,7 +232,7 @@
    1.13              let
    1.14                val _ =
    1.15                  if verbose then
    1.16 -                  Output.urgent_message ("Trying \"" ^ string_of_proof_method [] meth ^
    1.17 +                  Output.urgent_message ("Trying \"" ^ string_of_proof_method ctxt [] meth ^
    1.18                      "\" for " ^ string_of_time timeout ^ "...")
    1.19                  else
    1.20                    ()