avoid binding warning in Nitpick
authorblanchet
Wed Apr 22 23:26:14 2015 +0200 (2015-04-22)
changeset 601939274808fa020
parent 60192 39a2f9209a80
child 60194 fd2208491d59
avoid binding warning in Nitpick
src/Doc/Nitpick/document/root.tex
src/HOL/Tools/Nitpick/nitpick_model.ML
     1.1 --- a/src/Doc/Nitpick/document/root.tex	Wed Apr 22 19:52:29 2015 +0200
     1.2 +++ b/src/Doc/Nitpick/document/root.tex	Wed Apr 22 23:26:14 2015 +0200
     1.3 @@ -26,7 +26,8 @@
     1.4  \def\lparr{\mathopen{(\mkern-4mu\mid}}
     1.5  \def\rparr{\mathclose{\mid\mkern-4mu)}}
     1.6  
     1.7 -\def\unk{{?}}
     1.8 +%\def\unk{{?}}
     1.9 +\def\unk{{\_}}
    1.10  \def\unkef{(\lambda x.\; \unk)}
    1.11  \def\undef{(\lambda x.\; \_)}
    1.12  %\def\unr{\textit{others}}
    1.13 @@ -930,7 +931,7 @@
    1.14  \hbox{}\qquad Free variable: \nopagebreak \\
    1.15  \hbox{}\qquad\qquad $n = 1$ \\
    1.16  \hbox{}\qquad Constants: \nopagebreak \\
    1.17 -\hbox{}\qquad\qquad $\textit{even} = (λx. ?)(0 := True, 1 := False, 2 := True, 3 := False)$ \\
    1.18 +\hbox{}\qquad\qquad $\textit{even} = \unkef(0 := True, 1 := False, 2 := True, 3 := False)$ \\
    1.19  \hbox{}\qquad\qquad $\textit{odd}_{\textsl{base}} = {}$ \\
    1.20  \hbox{}\qquad\qquad\quad $\unkef(0 := \textit{False},\, 1 := \textit{True},\, 2 := \textit{False},\, 3 := \textit{False})$ \\
    1.21  \hbox{}\qquad\qquad $\textit{odd}_{\textsl{step}} = \unkef$\\
     2.1 --- a/src/HOL/Tools/Nitpick/nitpick_model.ML	Wed Apr 22 19:52:29 2015 +0200
     2.2 +++ b/src/HOL/Tools/Nitpick/nitpick_model.ML	Wed Apr 22 23:26:14 2015 +0200
     2.3 @@ -879,8 +879,11 @@
     2.4          t1 = t2
     2.5      end
     2.6  
     2.7 -fun pretty_term_auto_global ctxt t =
     2.8 +fun pretty_term_auto_global ctxt t0 =
     2.9    let
    2.10 +    val t = map_aterms (fn t as Const (s, _) =>
    2.11 +      if s = irrelevant orelse s = unknown then Term.dummy else t | t => t) t0
    2.12 +
    2.13      fun add_fake_const s =
    2.14        Sign.declare_const_global ((Binding.name s, @{typ 'a}), NoSyn)
    2.15        #> #2