--- a/src/HOL/SMT.thy Fri Oct 29 17:38:57 2010 +0200
+++ b/src/HOL/SMT.thy Fri Oct 29 18:17:04 2010 +0200
@@ -49,6 +49,20 @@
+subsection {* Distinctness *}
+
+text {*
+As an abbreviation for a quadratic number of inequalities, SMT solvers
+provide a built-in @{text distinct}. To avoid confusion with the
+already defined (and more general) @{term List.distinct}, a separate
+constant is defined.
+*}
+
+definition distinct :: "'a list \<Rightarrow> bool"
+where "distinct xs = List.distinct xs"
+
+
+
subsection {* Higher-order encoding *}
text {*
@@ -314,7 +328,7 @@
hide_type (open) pattern
hide_const Pattern term_eq
-hide_const (open) trigger pat nopat fun_app z3div z3mod
+hide_const (open) trigger pat nopat distinct fun_app z3div z3mod