diff -r c5a8b612e571 -r 0040bafffdef src/HOL/Tools/Nitpick/nitpick_preproc.ML
--- a/src/HOL/Tools/Nitpick/nitpick_preproc.ML	Thu Jul 01 16:54:42 2010 +0200
+++ b/src/HOL/Tools/Nitpick/nitpick_preproc.ML	Thu Jul 01 16:54:44 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 "*"}, Ts)) =
-        Type (@{type_name "*"}, map (box_type hol_ctxt InPair) 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 T = T
     fun add_boxed_types_for_var (z as (_, T)) (T', t') =
       case t' of
@@ -953,7 +953,7 @@
     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 "*"}, Ts) => fold (add_axioms_for_type depth) Ts
+      | Type (@{type_name Product_Type.prod}, Ts) => fold (add_axioms_for_type depth) Ts
       | @{typ prop} => I
       | @{typ bool} => I
       | @{typ unit} => I