# HG changeset patch
# User huffman
# Date 1321259105 -3600
# Node ID 8f32682f78fee1fcfe1bef6199e2235d4d250312
# Parent  cf937a9ce051ce11af05b2e5b87d8651a4e3579a# Parent  3387d482e0a98fdcc38ade2e71cd861f01d3b89b
merged

diff -r cf937a9ce051 -r 8f32682f78fe src/HOL/Rat.thy
--- a/src/HOL/Rat.thy	Sun Nov 13 19:30:35 2011 +0100
+++ b/src/HOL/Rat.thy	Mon Nov 14 09:25:05 2011 +0100
@@ -1210,8 +1210,7 @@
     (@{const_name inverse_rat_inst.inverse_rat}, @{const_name Nitpick.inverse_frac}),
     (@{const_name ord_rat_inst.less_rat}, @{const_name Nitpick.less_frac}),
     (@{const_name ord_rat_inst.less_eq_rat}, @{const_name Nitpick.less_eq_frac}),
-    (@{const_name field_char_0_class.of_rat}, @{const_name Nitpick.of_frac}),
-    (@{const_name field_char_0_class.Rats}, @{const_abbrev UNIV})]
+    (@{const_name field_char_0_class.of_rat}, @{const_name Nitpick.of_frac})]
 *}
 
 lemmas [nitpick_unfold] = inverse_rat_inst.inverse_rat
diff -r cf937a9ce051 -r 8f32682f78fe src/HOL/Tools/Nitpick/nitpick_model.ML
--- a/src/HOL/Tools/Nitpick/nitpick_model.ML	Sun Nov 13 19:30:35 2011 +0100
+++ b/src/HOL/Tools/Nitpick/nitpick_model.ML	Mon Nov 14 09:25:05 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