# HG changeset patch
# User blanchet
# Date 1256321665 -7200
# Node ID c56c627dae19f79e695e316f7eec800be621f92a
# Parent  6c9b2a94a69c147f0bf9f01958bd86ae9b5e67ca
be somewhat more liberal in Nitpick about which types may occur in formulas

diff -r 6c9b2a94a69c -r c56c627dae19 src/HOL/Tools/Nitpick/nitpick_hol.ML
--- 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)) =>