fixed a typo that caused the preference of non-random modes to be ignored
authorbulwahn
Tue, 28 Sep 2010 11:59:48 +0200
changeset 39993e6a370d35f45
parent 39987 150f831ce4a3
child 39994 c2a76ec6e2d9
fixed a typo that caused the preference of non-random modes to be ignored
src/HOL/Tools/Predicate_Compile/predicate_compile_core.ML
     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),