fixed soundness bug / type error in handling of unpolarized (co)inductive predicates in Nitpick
authorblanchet
Tue Nov 24 10:33:02 2009 +0100 (2009-11-24)
changeset 338798dfc55999130
parent 33878 85102f57b4a8
child 33880 6cc01403f78a
fixed soundness bug / type error in handling of unpolarized (co)inductive predicates in Nitpick
src/HOL/Tools/Nitpick/nitpick_hol.ML
     1.1 --- a/src/HOL/Tools/Nitpick/nitpick_hol.ML	Tue Nov 24 10:31:01 2009 +0100
     1.2 +++ b/src/HOL/Tools/Nitpick/nitpick_hol.ML	Tue Nov 24 10:33:02 2009 +0100
     1.3 @@ -2471,7 +2471,7 @@
     1.4                         list_comb (f (),
     1.5                                    map Bound (length trunk_arg_Ts - 1 downto 0))
     1.6                     in
     1.7 -                     List.foldl absdummy
     1.8 +                     List.foldr absdummy
     1.9                                  (Const (set_oper, [set_T, set_T] ---> set_T)
    1.10                                          $ app pos $ app neg) trunk_arg_Ts
    1.11                     end