src/Tools/Metis/src/Rewrite.sml

--- a/src/Tools/Metis/src/Rewrite.sml	Wed Sep 22 22:28:56 2021 +0200
+++ b/src/Tools/Metis/src/Rewrite.sml	Thu Sep 23 11:30:49 2021 +0200
@@ -364,7 +364,8 @@
             val lits = LiteralSet.add lits lit'
           in
             if Literal.equal lit lit' then (changed,lneq,lits,th)
-            else (true, lneq, lits, Thm.resolve lit th litTh)
+            else (true, lneq, lits,
+                  if Thm.member lit th then Thm.resolve lit th litTh else th)
           end
 
       fun rewr_neq_lits lits th =
@@ -411,7 +412,12 @@
     in
       result
     end
-    handle Error err => raise Error ("Rewrite.rewriteIdRule':\n" ^ err);
+    handle Error err =>
+      raise Error ("Rewrite.rewriteIdRule':\n" ^
+                   "th = " ^ Thm.toString th ^ "\n" ^ err)
+         | Bug bug =>
+      raise Bug ("Rewrite.rewriteIdRule':\n" ^
+                 "th = " ^ Thm.toString th ^ "\n" ^ bug);
 *)
 
 fun rewrIdConv (Rewrite {known,redexes,...}) order =