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