src/HOL/Tools/Nitpick/nitpick_model.ML
changeset 39360 cdf2c3341422
parent 39359 6f49c7fbb1b1
child 40132 7ee65dbffa31
     1.1 --- a/src/HOL/Tools/Nitpick/nitpick_model.ML	Tue Sep 14 13:24:18 2010 +0200
     1.2 +++ b/src/HOL/Tools/Nitpick/nitpick_model.ML	Tue Sep 14 13:44:43 2010 +0200
     1.3 @@ -816,16 +816,6 @@
     1.4           let
     1.5             val t = nth evals (the (Int.fromString (unprefix eval_prefix s)))
     1.6           in (t, format_term_type thy def_table formats t) end
     1.7 -       else if s = @{const_name undefined_fast_The} then
     1.8 -         (Const (nitpick_prefix ^ "The fallback", T),
     1.9 -          format_type default_format
    1.10 -                      (lookup_format thy def_table formats
    1.11 -                           (Const (@{const_name The}, (T --> bool_T) --> T))) T)
    1.12 -       else if s = @{const_name undefined_fast_Eps} then
    1.13 -         (Const (nitpick_prefix ^ "Eps fallback", T),
    1.14 -          format_type default_format
    1.15 -                      (lookup_format thy def_table formats
    1.16 -                           (Const (@{const_name Eps}, (T --> bool_T) --> T))) T)
    1.17         else
    1.18           let val t = Const (original_name s, T) in
    1.19             (t, format_term_type thy def_table formats t)