# HG changeset patch
# User haftmann
# Date 1259947170 -3600
# Node ID 901001414358e3b477dec2e92bbe41d263f89b03
# Parent  6e77ca6d3a8f8293d6799f1d319166481c36cb8e
tuned code setup

diff -r 6e77ca6d3a8f -r 901001414358 src/HOL/Predicate.thy
--- 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