changeset 50163 | c62ce309dc26 |
parent 49358 | 0fa351b1bd14 |
child 50201 | c26369c9eda6 |
--- a/src/HOL/Tools/Nitpick/nitpick.ML Thu Nov 22 12:22:03 2012 +0100 +++ b/src/HOL/Tools/Nitpick/nitpick.ML Thu Nov 22 13:21:02 2012 +0100 @@ -470,7 +470,7 @@ pprint_nt (fn () => Pretty.blk (0, pstrs "Hint: To check that the induction hypothesis is \ \general enough, try this command: " @ - [Pretty.mark Isabelle_Markup.sendback (Pretty.blk (0, + [Pretty.mark (Sendback.make_markup ()) (Pretty.blk (0, pstrs ("nitpick [non_std, show_all]")))] @ pstrs ".")) else ()