From 4ee759fc77b1631673ecc034c4ce9a1405ee4ec1 Mon Sep 17 00:00:00 2001 From: Michael Norrish Date: Thu, 3 Oct 2024 16:28:08 +1000 Subject: [PATCH] Reinstate old behaviour when rewrites compete MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit 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 cfa24e268b 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 | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/marker/markerLib.sml b/src/marker/markerLib.sml index 730a4c9993..15193fdb50 100644 --- a/src/marker/markerLib.sml +++ b/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)) =