--- 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$\\
--- 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