--- a/src/HOL/Tools/Nitpick/nitpick_preproc.ML Tue Aug 03 21:37:12 2010 +0200
+++ b/src/HOL/Tools/Nitpick/nitpick_preproc.ML Wed Aug 04 10:39:35 2010 +0200
@@ -132,8 +132,8 @@
let
fun box_relational_operator_type (Type (@{type_name fun}, Ts)) =
Type (@{type_name fun}, map box_relational_operator_type Ts)
- | box_relational_operator_type (Type (@{type_name Product_Type.prod}, Ts)) =
- Type (@{type_name Product_Type.prod}, map (box_type hol_ctxt InPair) Ts)
+ | box_relational_operator_type (Type (@{type_name prod}, Ts)) =
+ Type (@{type_name prod}, map (box_type hol_ctxt InPair) Ts)
| box_relational_operator_type T = T
fun add_boxed_types_for_var (z as (_, T)) (T', t') =
case t' of
@@ -1000,10 +1000,9 @@
and add_axioms_for_type depth T =
case T of
Type (@{type_name fun}, Ts) => fold (add_axioms_for_type depth) Ts
- | Type (@{type_name Product_Type.prod}, Ts) => fold (add_axioms_for_type depth) Ts
+ | Type (@{type_name prod}, Ts) => fold (add_axioms_for_type depth) Ts
| @{typ prop} => I
| @{typ bool} => I
- | @{typ unit} => I
| TFree (_, S) => add_axioms_for_sort depth T S
| TVar (_, S) => add_axioms_for_sort depth T S
| Type (z as (_, Ts)) =>