src/HOL/Tools/Nitpick/nitpick_mono.ML
changeset 41014 e538a4f9dd86
parent 41013 117345744f44
child 41016 343cdf923c02
     1.1 --- a/src/HOL/Tools/Nitpick/nitpick_mono.ML	Mon Dec 06 13:33:09 2010 +0100
     1.2 +++ b/src/HOL/Tools/Nitpick/nitpick_mono.ML	Mon Dec 06 13:33:09 2010 +0100
     1.3 @@ -800,11 +800,11 @@
     1.4      fun do_equals T (gamma, cset) =
     1.5        let
     1.6          val M = mtype_for (domain_type T)
     1.7 -        val aa = V (Unsynchronized.inc max_fresh)
     1.8 +        val x = Unsynchronized.inc max_fresh
     1.9        in
    1.10 -        (MFun (M, A Gen, MFun (M, aa, mtype_for (nth_range_type 2 T))),
    1.11 +        (MFun (M, A Gen, MFun (M, V x, mtype_for (nth_range_type 2 T))),
    1.12           (gamma, cset |> add_mtype_is_concrete [] M
    1.13 -                      |> add_annotation_atom_comp Leq [] (A Fls) aa))
    1.14 +                      |> add_annotation_atom_comp Leq [] (A Fls) (V x)))
    1.15        end
    1.16      fun do_robust_set_operation T (gamma, cset) =
    1.17        let
    1.18 @@ -980,8 +980,13 @@
    1.19                SOME t' =>
    1.20                let
    1.21                  val M = mtype_for T
    1.22 -                val (m', accum) = do_term t' (accum |>> push_bound (A Fls) T M)
    1.23 -              in (MAbs (s, T, M, A Fls, m'), accum |>> pop_bound) end
    1.24 +                val x = Unsynchronized.inc max_fresh
    1.25 +                val (m', accum) = do_term t' (accum |>> push_bound (V x) T M)
    1.26 +              in
    1.27 +                (MAbs (s, T, M, V x, m'),
    1.28 +                 accum |>> pop_bound
    1.29 +                       ||> add_annotation_atom_comp Leq [] (A Fls) (V x))
    1.30 +              end
    1.31              | NONE =>
    1.32                ((case t' of
    1.33                    t1' $ Bound 0 =>
    1.34 @@ -999,10 +1004,10 @@
    1.35                 handle SAME () =>
    1.36                        let
    1.37                          val M = mtype_for T
    1.38 -                        val aa = V (Unsynchronized.inc max_fresh)
    1.39 +                        val x = Unsynchronized.inc max_fresh
    1.40                          val (m', accum) =
    1.41 -                          do_term t' (accum |>> push_bound aa T M)
    1.42 -                      in (MAbs (s, T, M, aa, m'), accum |>> pop_bound) end))
    1.43 +                          do_term t' (accum |>> push_bound (V x) T M)
    1.44 +                      in (MAbs (s, T, M, V x, m'), accum |>> pop_bound) end))
    1.45           | @{const Not} $ t1 => do_connect imp_triple t1 @{const False} accum
    1.46           | @{const conj} $ t1 $ t2 => do_connect conj_triple t1 t2 accum
    1.47           | @{const disj} $ t1 $ t2 => do_connect disj_triple t1 t2 accum
    1.48 @@ -1051,14 +1056,14 @@
    1.49      val accum = accum ||> add_mtypes_equal M1 M2
    1.50      val body_M = fresh_mtype_for_type mdata false (nth_range_type 2 T)
    1.51      val m = MApp (MApp (MRaw (Const x,
    1.52 -                           MFun (M1, A Gen, MFun (M2, A Fls, body_M))), m1), m2)
    1.53 +                           MFun (M1, A Gen, MFun (M2, A Gen, body_M))), m1), m2)
    1.54    in
    1.55 -    (m, if def then
    1.56 -          let val (head_m, arg_ms) = strip_mcomb m1 in
    1.57 -            accum ||> force_gen_funs (length arg_ms) (mtype_of_mterm head_m)
    1.58 -          end
    1.59 -        else
    1.60 -          accum)
    1.61 +    (m, (if def then
    1.62 +           let val (head_m, arg_ms) = strip_mcomb m1 in
    1.63 +             accum ||> force_gen_funs (length arg_ms) (mtype_of_mterm head_m)
    1.64 +           end
    1.65 +         else
    1.66 +           accum))
    1.67    end
    1.68  
    1.69  fun consider_general_formula (mdata as {hol_ctxt = {ctxt, ...}, max_fresh,