| changeset 51070 | 6ca703425c01 |
| parent 49835 | 31f32ec4d766 |
| child 51551 | 88d1d19fb74f |
--- a/src/HOL/BNF/Tools/bnf_lfp.ML Mon Jan 28 22:37:58 2013 +0100 +++ b/src/HOL/BNF/Tools/bnf_lfp.ML Mon Jan 28 23:56:13 2013 +0100 @@ -152,7 +152,7 @@ val timer = time (timer "Extracted terms & thms"); (* nonemptiness check *) - fun new_wit X wit = subset (op =) (#I wit, (0 upto m - 1) @ map snd X); + fun new_wit X (wit: nonemptiness_witness) = subset (op =) (#I wit, (0 upto m - 1) @ map snd X); val all = m upto m + n - 1;