1.1 --- a/src/HOL/Tools/Predicate_Compile/predicate_compile_core.ML Tue Sep 28 09:54:07 2010 +0200
1.2 +++ b/src/HOL/Tools/Predicate_Compile/predicate_compile_core.ML Tue Sep 28 11:59:48 2010 +0200
1.3 @@ -1340,7 +1340,7 @@
1.4 (* prefer non-random modes *)
1.5 fun random_mode_ord ((t1, deriv1, mvars1), (t2, deriv2, mvars2)) =
1.6 int_ord (if random_mode_in_deriv modes t1 deriv1 then 1 else 0,
1.7 - if random_mode_in_deriv modes t1 deriv1 then 1 else 0)
1.8 + if random_mode_in_deriv modes t2 deriv2 then 1 else 0)
1.9 (* prefer modes with more input and less output *)
1.10 fun output_mode_ord ((t1, deriv1, mvars1), (t2, deriv2, mvars2)) =
1.11 int_ord (number_of_output_positions (head_mode_of deriv1),