# HG changeset patch
# User boehmes
# Date 1292831127 -3600
# Node ID 0a00fd2f535192c9ad5e5f05f9261896a52e782b
# Parent  528f5d00b5428816dc13dd362d01505cd97b6cd4
derived SMT solver classes override inherited properties (properties of derived classes have a higher priority than properties of base classes)

diff -r 528f5d00b542 -r 0a00fd2f5351 src/HOL/Tools/SMT/smt_utils.ML
--- a/src/HOL/Tools/SMT/smt_utils.ML	Mon Dec 20 08:17:23 2010 +0100
+++ b/src/HOL/Tools/SMT/smt_utils.ML	Mon Dec 20 08:45:27 2010 +0100
@@ -86,7 +86,8 @@
 
 type 'a dict = (class * 'a) Ord_List.T
 
-fun class_ord ((cs1, _), (cs2, _)) = list_ord fast_string_ord (cs1, cs2)
+fun class_ord ((cs1, _), (cs2, _)) =
+  rev_order (list_ord fast_string_ord (cs1, cs2))
 
 fun dict_insert (cs, x) d =
   if AList.defined (op =) d cs then d