--- a/src/HOL/Tools/Nitpick/nitpick_model.ML Sun Nov 13 20:28:22 2011 +0100
+++ b/src/HOL/Tools/Nitpick/nitpick_model.ML Sun Nov 13 20:28:22 2011 +0100
@@ -819,7 +819,9 @@
val t = nth evals (the (Int.fromString (unprefix eval_prefix s)))
in (t, format_term_type thy def_tables formats t) end
else
- let val t = Const (original_name s, T) in
+ (* The selector case can occur in conjunction with fractional types.
+ It's not pretty. *)
+ let val t = Const (s |> not (is_sel s) ? original_name, T) in
(t, format_term_type thy def_tables formats t)
end)
|>> map_types uniterize_unarize_unbox_etc_type