changeset 57992 | 2371bff894f9 |
parent 57964 | 3dfc1bf3ac3d |
child 58634 | 9f10d82e8188 |
--- a/src/HOL/Tools/Nitpick/nitpick_hol.ML Tue Aug 19 09:34:30 2014 +0200 +++ b/src/HOL/Tools/Nitpick/nitpick_hol.ML Tue Aug 19 09:34:41 2014 +0200 @@ -974,7 +974,7 @@ fun zero_const T = Const (@{const_name zero_class.zero}, T) fun suc_const T = Const (@{const_name Suc}, T --> T) -fun uncached_data_type_constrs ({thy, ctxt, ...} : hol_context) (T as Type (s, _)) = +fun uncached_data_type_constrs ({ctxt, ...} : hol_context) (T as Type (s, _)) = if is_interpreted_type s then [] else