Reinstate old behaviour when rewrites compete

If we have ⊢ x = e1 in the argument list and x = e2 as an assumption,
the theorem in the assumptions used to be chosen first by simp and
friends. The commit in cfa24e2 flipped this choice, but this flips
it back again. Of course, users shouldn't really be relying on this,
but at least one CakeML proof did, and in this case, there seems no
need to punish this.

src/marker/markerLib.sml

@@ -696,7 +696,7 @@ fun filter_then asms aslPs thltac (gl as (asl0,g)) =
       val asl = apply_aslPs (free_varsl (g::asl0)) aslPs
                             (filter (not o is_label) asl0)
     in
-      thltac (asms @ map ASSUME asl) gl
+      thltac (map ASSUME asl @ asms) gl
     end
 
 fun process_taclist_then {arg} thltac (gl as (asl,g)) =