# HG changeset patch
# User blanchet
# Date 1429737974 -7200
# Node ID 9274808fa020a1509faefc8255d91990a5c39c9f
# Parent  39a2f9209a80943e053b0bb443705e7549b0a525
avoid binding warning in Nitpick

diff -r 39a2f9209a80 -r 9274808fa020 src/Doc/Nitpick/document/root.tex
--- a/src/Doc/Nitpick/document/root.tex	Wed Apr 22 19:52:29 2015 +0200
+++ b/src/Doc/Nitpick/document/root.tex	Wed Apr 22 23:26:14 2015 +0200
@@ -26,7 +26,8 @@
 \def\lparr{\mathopen{(\mkern-4mu\mid}}
 \def\rparr{\mathclose{\mid\mkern-4mu)}}
 
-\def\unk{{?}}
+%\def\unk{{?}}
+\def\unk{{\_}}
 \def\unkef{(\lambda x.\; \unk)}
 \def\undef{(\lambda x.\; \_)}
 %\def\unr{\textit{others}}
@@ -930,7 +931,7 @@
 \hbox{}\qquad Free variable: \nopagebreak \\
 \hbox{}\qquad\qquad $n = 1$ \\
 \hbox{}\qquad Constants: \nopagebreak \\
-\hbox{}\qquad\qquad $\textit{even} = (λx. ?)(0 := True, 1 := False, 2 := True, 3 := False)$ \\
+\hbox{}\qquad\qquad $\textit{even} = \unkef(0 := True, 1 := False, 2 := True, 3 := False)$ \\
 \hbox{}\qquad\qquad $\textit{odd}_{\textsl{base}} = {}$ \\
 \hbox{}\qquad\qquad\quad $\unkef(0 := \textit{False},\, 1 := \textit{True},\, 2 := \textit{False},\, 3 := \textit{False})$ \\
 \hbox{}\qquad\qquad $\textit{odd}_{\textsl{step}} = \unkef$\\
diff -r 39a2f9209a80 -r 9274808fa020 src/HOL/Tools/Nitpick/nitpick_model.ML
--- a/src/HOL/Tools/Nitpick/nitpick_model.ML	Wed Apr 22 19:52:29 2015 +0200
+++ b/src/HOL/Tools/Nitpick/nitpick_model.ML	Wed Apr 22 23:26:14 2015 +0200
@@ -879,8 +879,11 @@
         t1 = t2
     end
 
-fun pretty_term_auto_global ctxt t =
+fun pretty_term_auto_global ctxt t0 =
   let
+    val t = map_aterms (fn t as Const (s, _) =>
+      if s = irrelevant orelse s = unknown then Term.dummy else t | t => t) t0
+
     fun add_fake_const s =
       Sign.declare_const_global ((Binding.name s, @{typ 'a}), NoSyn)
       #> #2