src/Pure/Isar/proof_context.ML

   in
     (case map_filter print_proof (dest_cases (SOME ctxt0) ctxt) of
       [] => ""
     | proofs =>
         "Proof outline with cases:\n" ^
-        Active.sendback_markup [Markup.padding_command]
-          (space_implode "\nnext\n" proofs ^ "\nqed"))
+        Active.sendback_markup_command (space_implode "\nnext\n" proofs ^ "\nqed"))
   end;
 
 
 (* core context *)