src/HOL/Tools/Sledgehammer/sledgehammer_reconstruct.ML

                    in string_of_int num_steps ^ plural_s num_steps end]
                 else [])
           in
             "\n\nStructured proof "
               ^ (commas msg |> not (null msg) ? enclose "(" ")")
-              ^ ":\n" ^ Markup.markup Markup.sendback isar_text
+              ^ ":\n" ^ Sendback.markup isar_text
           end
       end
     val isar_proof =
       if debug then
         isar_proof_of ()