--- 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"},