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