# HG changeset patch # User bulwahn # Date 1327575815 -3600 # Node ID 39fe503602fba638bc1948091b038421985c6375 # Parent 0fd9ab902b5a46d690201219770ba987d8cc5a09 evaluation of THE with a non-singleton set raises a Match exception during the evaluation to yield a potential counterexample in quickcheck. diff -r 0fd9ab902b5a -r 39fe503602fb src/HOL/Enum.thy --- a/src/HOL/Enum.thy Thu Jan 26 10:59:47 2012 +0100 +++ b/src/HOL/Enum.thy Thu Jan 26 12:03:35 2012 +0100 @@ -777,6 +777,7 @@ qed code_abort enum_the +code_const enum_the (Eval "(fn p => raise Match)") subsection {* Further operations on finite types *}