src/HOL/Tools/Nitpick/nitpick_scope.ML
changeset 41052 3db267a01c1d
parent 39118 12f3788be67b
child 41991 ea02b9ee3085
     1.1 --- a/src/HOL/Tools/Nitpick/nitpick_scope.ML	Tue Dec 07 11:56:01 2010 +0100
     1.2 +++ b/src/HOL/Tools/Nitpick/nitpick_scope.ML	Tue Dec 07 11:56:53 2010 +0100
     1.3 @@ -112,8 +112,6 @@
     1.4  
     1.5  fun is_complete_type dtypes facto (Type (@{type_name fun}, [T1, T2])) =
     1.6      is_concrete_type dtypes facto T1 andalso is_complete_type dtypes facto T2
     1.7 -  | is_complete_type dtypes facto (Type (@{type_name fin_fun}, [T1, T2])) =
     1.8 -    is_exact_type dtypes facto T1 andalso is_complete_type dtypes facto T2
     1.9    | is_complete_type dtypes facto (Type (@{type_name prod}, Ts)) =
    1.10      forall (is_complete_type dtypes facto) Ts
    1.11    | is_complete_type dtypes facto T =
    1.12 @@ -122,8 +120,6 @@
    1.13      handle Option.Option => true
    1.14  and is_concrete_type dtypes facto (Type (@{type_name fun}, [T1, T2])) =
    1.15      is_complete_type dtypes facto T1 andalso is_concrete_type dtypes facto T2
    1.16 -  | is_concrete_type dtypes facto (Type (@{type_name fin_fun}, [_, T2])) =
    1.17 -    is_concrete_type dtypes facto T2
    1.18    | is_concrete_type dtypes facto (Type (@{type_name prod}, Ts)) =
    1.19      forall (is_concrete_type dtypes facto) Ts
    1.20    | is_concrete_type dtypes facto T =