1.1 --- a/src/HOL/Tools/Nitpick/nitpick_hol.ML	Tue Jun 01 10:32:29 2010 +0200
     1.2 +++ b/src/HOL/Tools/Nitpick/nitpick_hol.ML	Tue Jun 01 10:40:23 2010 +0200
     1.3 @@ -533,9 +533,10 @@
     1.4                              |> Logic.varify_global,
     1.5              set_name = @{const_name Frac}, Abs_inverse = NONE, Rep_inverse = NONE}
     1.6      else case Typedef.get_info ctxt s of
     1.7 -      (* ### multiple *)
     1.8 -      [({abs_type, rep_type, Abs_name, Rep_name, ...},
     1.9 -        {set_def, Rep, Abs_inverse, Rep_inverse, ...})] =>
    1.10 +      (* When several entries are returned, it shouldn't matter much which one
    1.11 +         we take (according to Florian Haftmann). *)
    1.12 +      ({abs_type, rep_type, Abs_name, Rep_name, ...},
    1.13 +       {set_def, Rep, Abs_inverse, Rep_inverse, ...}) :: _ =>
    1.14        SOME {abs_type = abs_type, rep_type = rep_type, Abs_name = Abs_name,
    1.15              Rep_name = Rep_name, set_def = set_def, prop_of_Rep = prop_of Rep,
    1.16              set_name = set_prefix ^ s, Abs_inverse = SOME Abs_inverse,