avoid confusing selector output
authorblanchet
Sun Nov 13 20:28:22 2011 +0100 (2011-11-13)
changeset 454793387d482e0a9
parent 45478 8e299034eab4
child 45482 8f32682f78fe
avoid confusing selector output
src/HOL/Tools/Nitpick/nitpick_model.ML
     1.1 --- a/src/HOL/Tools/Nitpick/nitpick_model.ML	Sun Nov 13 20:28:22 2011 +0100
     1.2 +++ b/src/HOL/Tools/Nitpick/nitpick_model.ML	Sun Nov 13 20:28:22 2011 +0100
     1.3 @@ -819,7 +819,9 @@
     1.4             val t = nth evals (the (Int.fromString (unprefix eval_prefix s)))
     1.5           in (t, format_term_type thy def_tables formats t) end
     1.6         else
     1.7 -         let val t = Const (original_name s, T) in
     1.8 +         (* The selector case can occur in conjunction with fractional types.
     1.9 +            It's not pretty. *)
    1.10 +         let val t = Const (s |> not (is_sel s) ? original_name, T) in
    1.11             (t, format_term_type thy def_tables formats t)
    1.12           end)
    1.13        |>> map_types uniterize_unarize_unbox_etc_type