--- a/src/HOL/Tools/Nitpick/nitpick_hol.ML Sat Mar 27 18:43:11 2010 +0100
+++ b/src/HOL/Tools/Nitpick/nitpick_hol.ML Sat Mar 27 21:38:38 2010 +0100
@@ -570,8 +570,8 @@
set_name = @{const_name Frac}, Abs_inverse = NONE, Rep_inverse = NONE}
else case Typedef.get_info_global thy s of
(* FIXME handle multiple typedef interpretations (!??) *)
- [{abs_type, rep_type, Abs_name, Rep_name, set_def, Rep, Abs_inverse,
- Rep_inverse, ...}] =>
+ [({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,