--- a/src/HOL/Predicate.thy Sun Nov 29 12:56:30 2009 +1100
+++ b/src/HOL/Predicate.thy Fri Dec 04 18:19:30 2009 +0100
@@ -831,6 +831,8 @@
lemma the_eq[code]: "the A = singleton (\<lambda>x. not_unique A) A"
by (auto simp add: the_def singleton_def not_unique_def)
+code_abort not_unique
+
ML {*
signature PREDICATE =
sig
@@ -876,8 +878,6 @@
code_const Seq and Empty and Insert and Join
(Eval "Predicate.Seq" and "Predicate.Empty" and "Predicate.Insert/ (_,/ _)" and "Predicate.Join/ (_,/ _)")
-code_abort not_unique
-
no_notation
inf (infixl "\<sqinter>" 70) and
sup (infixl "\<squnion>" 65) and