diff -r 542f2c6da692 -r 3f494c048142 src/HOL/Tools/Nitpick/nitpick_hol.ML
--- a/src/HOL/Tools/Nitpick/nitpick_hol.ML	Fri Dec 18 14:23:11 2015 +0100
+++ b/src/HOL/Tools/Nitpick/nitpick_hol.ML	Sat Dec 19 20:02:51 2015 +0100
@@ -575,11 +575,6 @@
 fun dest_n_tuple 1 t = [t]
   | dest_n_tuple n t = HOLogic.dest_prod t ||> dest_n_tuple (n - 1) |> op ::
 
-type typedef_info =
-  {rep_type: typ, abs_type: typ, Rep_name: string, Abs_name: string,
-   prop_of_Rep: thm, set_name: string option, Abs_inverse: thm option,
-   Rep_inverse: thm option}
-
 fun typedef_info ctxt s =
   if is_frac_type ctxt (Type (s, [])) then
     SOME {abs_type = Type (s, []), rep_type = @{typ "int * int"},