# HG changeset patch
# User blanchet
# Date 1275381623 -7200
# Node ID 40bebf3d6cc016ab050e9c51b915ed2c0d1aefe5
# Parent  eddca6e94b784d1437a0d1be97a47357288e209b
make Nitpick handle multiple typedef entries for same typedef

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