src/HOL/Tools/Nitpick/nitpick_mono.ML
changeset 39316 b6c4385ab400
parent 38864 4abe644fcea5
child 39342 1a0e6f16a91b
     1.1 --- a/src/HOL/Tools/Nitpick/nitpick_mono.ML	Sat Sep 11 10:13:51 2010 +0200
     1.2 +++ b/src/HOL/Tools/Nitpick/nitpick_mono.ML	Sat Sep 11 10:20:25 2010 +0200
     1.3 @@ -660,7 +660,7 @@
     1.4                  |>> curry3 MFun bool_M (S Minus)
     1.5                | @{const_name Pair} => do_pair_constr T accum
     1.6                | @{const_name fst} => do_nth_pair_sel 0 T accum
     1.7 -              | @{const_name snd} => do_nth_pair_sel 1 T accum 
     1.8 +              | @{const_name snd} => do_nth_pair_sel 1 T accum
     1.9                | @{const_name Id} =>
    1.10                  (MFun (mtype_for (domain_type T), S Minus, bool_M), accum)
    1.11                | @{const_name converse} =>
    1.12 @@ -894,7 +894,7 @@
    1.13                 in
    1.14                   (MApp (MApp (MRaw (t0, mtype_for (fastype_of t0)), m1), m2),
    1.15                    accum)
    1.16 -               end 
    1.17 +               end
    1.18               else
    1.19                 do_term t accum
    1.20             | _ => do_term t accum)
    1.21 @@ -1105,7 +1105,7 @@
    1.22                val (T1, T2) = pairself (curry fastype_of1 new_Ts) (t1, t2)
    1.23                val (t1', T2') =
    1.24                  case T1 of
    1.25 -                  Type (s, [T11, T12]) => 
    1.26 +                  Type (s, [T11, T12]) =>
    1.27                    (if s = @{type_name fin_fun} then
    1.28                       select_nth_constr_arg ctxt stds (fin_fun_constr T11 T12) t1
    1.29                                             0 (T11 --> T12)