
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 \<in> S \<and> 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




