src/HOL/Tools/Sledgehammer/sledgehammer_prover_atp.ML

               (if atp_proof_prefers_lifting atp_proof then liftingN else hide_lamsN)
         in
           (used_facts,
            Lazy.lazy (fn () =>
              let val used_pairs = used_from |> filter_used_facts false used_facts in
-               play_one_line_proof mode verbose preplay_timeout used_pairs state subgoal (hd meths)
-                 meths
+               play_one_line_proof mode debug verbose preplay_timeout used_pairs state subgoal
+                 (hd meths) meths
              end),
            fn preplay =>
               let
                 val _ = if verbose then Output.urgent_message "Generating proof text..." else ()
                 fun isar_params () =