fix soundness bug in "uncurry" option of Nitpick
authorblanchet
Tue Nov 24 18:35:21 2009 +0100 (2009-11-24)
changeset 3389148463e8876bd
parent 33890 a87ad4be59a4
child 33892 3937da7e13ea
fix soundness bug in "uncurry" option of Nitpick
src/HOL/Tools/Nitpick/nitpick_hol.ML
     1.1 --- a/src/HOL/Tools/Nitpick/nitpick_hol.ML	Tue Nov 24 17:54:33 2009 +0100
     1.2 +++ b/src/HOL/Tools/Nitpick/nitpick_hol.ML	Tue Nov 24 18:35:21 2009 +0100
     1.3 @@ -2647,7 +2647,7 @@
     1.4          let val table = aux t2 [] table in aux t1 (t2 :: args) table end
     1.5        | aux (Abs (_, _, t')) _ table = aux t' [] table
     1.6        | aux (t as Const (x as (s, _))) args table =
     1.7 -        if is_built_in_const false x orelse is_constr_like thy x orelse is_sel s
     1.8 +        if is_built_in_const true x orelse is_constr_like thy x orelse is_sel s
     1.9             orelse s = @{const_name Sigma} then
    1.10            table
    1.11          else