--- a/src/HOL/Tools/Nitpick/nitpick_scope.ML Thu Jul 01 16:54:42 2010 +0200
+++ b/src/HOL/Tools/Nitpick/nitpick_scope.ML Thu Jul 01 16:54:44 2010 +0200
@@ -107,7 +107,7 @@
is_concrete_type dtypes facto T1 andalso is_complete_type dtypes facto T2
| is_complete_type dtypes facto (Type (@{type_name fin_fun}, [T1, T2])) =
is_exact_type dtypes facto T1 andalso is_complete_type dtypes facto T2
- | is_complete_type dtypes facto (Type (@{type_name "*"}, Ts)) =
+ | is_complete_type dtypes facto (Type (@{type_name Product_Type.prod}, Ts)) =
forall (is_complete_type dtypes facto) Ts
| is_complete_type dtypes facto T =
not (is_integer_like_type T) andalso not (is_bit_type T) andalso
@@ -117,7 +117,7 @@
is_complete_type dtypes facto T1 andalso is_concrete_type dtypes facto T2
| is_concrete_type dtypes facto (Type (@{type_name fin_fun}, [_, T2])) =
is_concrete_type dtypes facto T2
- | is_concrete_type dtypes facto (Type (@{type_name "*"}, Ts)) =
+ | is_concrete_type dtypes facto (Type (@{type_name Product_Type.prod}, Ts)) =
forall (is_concrete_type dtypes facto) Ts
| is_concrete_type dtypes facto T =
fun_from_pair (#concrete (the (datatype_spec dtypes T))) facto