src/HOL/Tools/Nitpick/nitpick_model.ML
changeset 60193 9274808fa020
parent 60187 0043ad2a770f
child 60310 932221b62e89
     1.1 --- a/src/HOL/Tools/Nitpick/nitpick_model.ML	Wed Apr 22 19:52:29 2015 +0200
     1.2 +++ b/src/HOL/Tools/Nitpick/nitpick_model.ML	Wed Apr 22 23:26:14 2015 +0200
     1.3 @@ -879,8 +879,11 @@
     1.4          t1 = t2
     1.5      end
     1.6  
     1.7 -fun pretty_term_auto_global ctxt t =
     1.8 +fun pretty_term_auto_global ctxt t0 =
     1.9    let
    1.10 +    val t = map_aterms (fn t as Const (s, _) =>
    1.11 +      if s = irrelevant orelse s = unknown then Term.dummy else t | t => t) t0
    1.12 +
    1.13      fun add_fake_const s =
    1.14        Sign.declare_const_global ((Binding.name s, @{typ 'a}), NoSyn)
    1.15        #> #2