# HG changeset patch # User blanchet # Date 1259084121 -3600 # Node ID 48463e8876bde4ea72040b013e94b1c9620efcfa # Parent a87ad4be59a4771e9628c2229b29e64e452f9dd5 fix soundness bug in "uncurry" option of Nitpick diff -r a87ad4be59a4 -r 48463e8876bd src/HOL/Tools/Nitpick/nitpick_hol.ML --- a/src/HOL/Tools/Nitpick/nitpick_hol.ML Tue Nov 24 17:54:33 2009 +0100 +++ b/src/HOL/Tools/Nitpick/nitpick_hol.ML Tue Nov 24 18:35:21 2009 +0100 @@ -2647,7 +2647,7 @@ let val table = aux t2 [] table in aux t1 (t2 :: args) table end | aux (Abs (_, _, t')) _ table = aux t' [] table | aux (t as Const (x as (s, _))) args table = - if is_built_in_const false x orelse is_constr_like thy x orelse is_sel s + if is_built_in_const true x orelse is_constr_like thy x orelse is_sel s orelse s = @{const_name Sigma} then table else