src/HOL/Tools/Nitpick/nitpick_model.ML
changeset 35388 42d39948cace
parent 35385 29f81babefd7
child 35402 115a5a95710a
     1.1 --- a/src/HOL/Tools/Nitpick/nitpick_model.ML	Fri Feb 26 16:50:09 2010 +0100
     1.2 +++ b/src/HOL/Tools/Nitpick/nitpick_model.ML	Fri Feb 26 18:38:23 2010 +0100
     1.3 @@ -281,7 +281,7 @@
     1.4               js 0
     1.5        end
     1.6      (* bool -> typ -> typ -> (term * term) list -> term *)
     1.7 -    fun make_set maybe_opt T1 T2 =
     1.8 +    fun make_set maybe_opt T1 T2 tps =
     1.9        let
    1.10          val empty_const = Const (@{const_name Set.empty}, T1 --> T2)
    1.11          val insert_const = Const (@{const_name insert},
    1.12 @@ -293,13 +293,20 @@
    1.13              else
    1.14                empty_const
    1.15            | aux ((t1, t2) :: zs) =
    1.16 -            aux zs |> t2 <> @{const False}
    1.17 -                      ? curry (op $) (insert_const
    1.18 -                                      $ (t1 |> t2 <> @{const True}
    1.19 -                                               ? curry (op $)
    1.20 -                                                       (Const (maybe_name,
    1.21 -                                                               T1 --> T1))))
    1.22 -      in aux end
    1.23 +            aux zs
    1.24 +            |> t2 <> @{const False}
    1.25 +               ? curry (op $)
    1.26 +                       (insert_const
    1.27 +                        $ (t1 |> t2 <> @{const True}
    1.28 +                                 ? curry (op $)
    1.29 +                                         (Const (maybe_name, T1 --> T1))))
    1.30 +      in
    1.31 +        if forall (fn (_, t) => t <> @{const True} andalso t <> @{const False})
    1.32 +                  tps then
    1.33 +          Const (unknown, T1 --> T2)
    1.34 +        else
    1.35 +          aux tps
    1.36 +      end
    1.37      (* typ -> typ -> typ -> (term * term) list -> term *)
    1.38      fun make_map T1 T2 T2' =
    1.39        let