# HG changeset patch
# User bulwahn
# Date 1285667988 -7200
# Node ID e6a370d35f45cbc516b662f55a1f46d2ada7bd5b
# Parent  150f831ce4a339a3717d10a69ae447cb04005f4f
fixed a typo that caused the preference of non-random modes to be ignored

diff -r 150f831ce4a3 -r e6a370d35f45 src/HOL/Tools/Predicate_Compile/predicate_compile_core.ML
--- a/src/HOL/Tools/Predicate_Compile/predicate_compile_core.ML	Tue Sep 28 09:54:07 2010 +0200
+++ b/src/HOL/Tools/Predicate_Compile/predicate_compile_core.ML	Tue Sep 28 11:59:48 2010 +0200
@@ -1340,7 +1340,7 @@
     (* prefer non-random modes *)
     fun random_mode_ord ((t1, deriv1, mvars1), (t2, deriv2, mvars2)) =
       int_ord (if random_mode_in_deriv modes t1 deriv1 then 1 else 0,
-        if random_mode_in_deriv modes t1 deriv1 then 1 else 0)
+               if random_mode_in_deriv modes t2 deriv2 then 1 else 0)
     (* prefer modes with more input and less output *)
     fun output_mode_ord ((t1, deriv1, mvars1), (t2, deriv2, mvars2)) =
       int_ord (number_of_output_positions (head_mode_of deriv1),