--- a/src/HOL/Tools/Nitpick/nitpick_hol.ML Fri Oct 23 20:13:33 2009 +0200
+++ b/src/HOL/Tools/Nitpick/nitpick_hol.ML Fri Oct 23 20:14:25 2009 +0200
@@ -3059,10 +3059,6 @@
| @{typ prop} => I
| @{typ bool} => I
| @{typ unit} => I
- | Type (@{type_name Datatype.node}, _) =>
- raise NOT_SUPPORTED "internal datatype node type"
- | Type (@{type_name tuple_isomorphism}, _) =>
- raise NOT_SUPPORTED "internal record tuple type"
| TFree (_, S) => add_axioms_for_sort depth T S
| TVar (_, S) => add_axioms_for_sort depth T S
| Type (z as (_, Ts)) =>