# HG changeset patch
# User wenzelm
# Date 1353927596 -3600
# Node ID 4fb06c22c5ec9841dbdfbd1409f6357fc1e05a69
# Parent  2a3d6d760629ea4726d037a96af68eb0fda0400e
tuned signature;

diff -r 2a3d6d760629 -r 4fb06c22c5ec src/HOL/Tools/Nitpick/nitpick.ML
--- a/src/HOL/Tools/Nitpick/nitpick.ML	Mon Nov 26 11:42:16 2012 +0100
+++ b/src/HOL/Tools/Nitpick/nitpick.ML	Mon Nov 26 11:59:56 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 (Sendback.make_markup ()) (Pretty.blk (0,
+                  [Pretty.mark (Sendback.make_markup {implicit = false}) (Pretty.blk (0,
                        pstrs ("nitpick [non_std, show_all]")))] @ pstrs "."))
             else
               ()
diff -r 2a3d6d760629 -r 4fb06c22c5ec src/Pure/PIDE/sendback.ML
--- a/src/Pure/PIDE/sendback.ML	Mon Nov 26 11:42:16 2012 +0100
+++ b/src/Pure/PIDE/sendback.ML	Mon Nov 26 11:59:56 2012 +0100
@@ -7,25 +7,26 @@
 
 signature SENDBACK =
 sig
-  val make_markup: unit -> Markup.T
+  val make_markup: {implicit: bool} -> Markup.T
+  val markup_implicit: string -> string
   val markup: string -> string
-  val markup_implicit: string -> string
 end;
 
 structure Sendback: SENDBACK =
 struct
 
-fun make_markup () =
-  let
-    val props =
-      (case Position.get_id (Position.thread_data ()) of
-        SOME id => [(Markup.idN, id)]
-      | NONE => []);
-  in Markup.properties props Markup.sendback end;
+fun make_markup {implicit} =
+  if implicit then Markup.sendback
+  else
+    let
+      val props =
+        (case Position.get_id (Position.thread_data ()) of
+          SOME id => [(Markup.idN, id)]
+        | NONE => []);
+    in Markup.properties props Markup.sendback end;
 
-fun markup s = Markup.markup (make_markup ()) s;
-
-fun markup_implicit s = Markup.markup Markup.sendback s;
+fun markup_implicit s = Markup.markup (make_markup {implicit = true}) s;
+fun markup s = Markup.markup (make_markup {implicit = false}) s;
 
 end;