# HG changeset patch
# User wenzelm
# Date 1729683011 -7200
# Node ID 3b49bf00c8e44e37a25d17a010a4bbb068b93873
# Parent  47b95e6af3c88da3fe972c063f6717d53b7543db
tuned;

diff -r 47b95e6af3c8 -r 3b49bf00c8e4 src/Pure/Syntax/ast.ML
--- a/src/Pure/Syntax/ast.ML	Wed Oct 23 13:03:49 2024 +0200
+++ b/src/Pure/Syntax/ast.ML	Wed Oct 23 13:30:11 2024 +0200
@@ -234,6 +234,10 @@
     val changes = Unsynchronized.ref 0;
     val passes = Unsynchronized.ref 0;
 
+    fun test_changes () =
+      let val old_changes = ! changes
+      in fn () => old_changes <> ! changes end;
+
     fun rewrite1 ast (lhs, rhs) =
       (case match p ast lhs of
         NONE => (Unsynchronized.inc matches_failed; NONE)
@@ -255,17 +259,17 @@
       (case norm1 ast of
         Appl subs =>
           let
-            val old_changes = ! changes;
+            val changed = test_changes ();
             val ast' = Appl (map norm2 subs);
-          in if old_changes = ! changes then ast' else norm1 ast' end
+          in if changed () then norm1 ast' else ast' end
       | atomic => atomic);
 
     fun norm ast =
       let
-        val old_changes = ! changes;
+        val changed = test_changes ();
         val ast' = norm2 ast;
         val _ = Unsynchronized.inc passes;
-      in if old_changes = ! changes then ast' else norm ast' end;
+      in if changed () then norm ast' else ast' end;
 
 
     val _ = tracing_if trace (fn () => message "pre:" (pretty_ast pre_ast));