--- a/src/HOL/Tools/Nitpick/nitpick_scope.ML Tue Aug 03 21:37:12 2010 +0200
+++ b/src/HOL/Tools/Nitpick/nitpick_scope.ML Wed Aug 04 10:39:35 2010 +0200
@@ -114,7 +114,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 Product_Type.prod}, Ts)) =
+ | is_complete_type dtypes facto (Type (@{type_name 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
@@ -124,7 +124,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 Product_Type.prod}, Ts)) =
+ | is_concrete_type dtypes facto (Type (@{type_name 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