src/HOL/Tools/Nitpick/nitpick.ML
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
               ()