src/HOL/Tools/Sledgehammer/sledgehammer_prover_smt.ML

   else
     NONE
 
 fun weight_smt_fact ctxt num_facts ((info, th), j) =
   let val thy = Proof_Context.theory_of ctxt in
-    (info, (smt_fact_weight ctxt j num_facts, th |> Thm.transfer thy))
+    (info, (smt_fact_weight ctxt j num_facts, Thm.transfer thy th (* TODO: needed? *)))
   end
 
 (* "SMT_Failure.Abnormal_Termination" carries the solver's return code. Until these are sorted out
    properly in the SMT module, we must interpret these here. *)
 val z3_failures =

       end
   in
     do_slice timeout 1 NONE Time.zeroTime
   end
 
-fun run_smt_solver mode name (params as {verbose, smt_proofs, preplay_timeout, ...})
+fun run_smt_solver mode name (params as {debug, verbose, smt_proofs, preplay_timeout, ...})
     minimize_command ({state, goal, subgoal, subgoal_count, factss, ...} : prover_problem) =
   let
     val thy = Proof.theory_of state
     val ctxt = Proof.context_of state
 

 
     val (preplay, message, message_tail) =
       (case outcome of
         NONE =>
         (Lazy.lazy (fn () =>
-           play_one_line_proof mode verbose preplay_timeout used_pairs state subgoal SMT_Method
-             (bunch_of_proof_methods (smt_proofs <> SOME false) false liftingN)),
+           play_one_line_proof mode debug verbose preplay_timeout used_pairs state subgoal
+             SMT_Method (bunch_of_proof_methods (smt_proofs <> SOME false) false liftingN)),
          fn preplay =>
             let
               val one_line_params =
                 (preplay, proof_banner mode name, used_facts,
                  choose_minimize_command thy params minimize_command name preplay, subgoal,