diff -r 4121d64fde90 -r cb892d835803 src/HOL/List.thy --- a/src/HOL/List.thy Wed Jan 01 01:05:46 2014 +0100 +++ b/src/HOL/List.thy Wed Jan 01 01:05:48 2014 +0100 @@ -6133,7 +6133,7 @@ definition "abort_Bleast S P = (LEAST x. x \ S \ P x)" -code_abort abort_Bleast +declare [[code abort: abort_Bleast]] lemma Bleast_code [code]: "Bleast (set xs) P = (case filter P (sort xs) of