be somewhat more liberal in Nitpick about which types may occur in formulas

--- 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)) =>