diff -r 4e6fc3336336 -r 07a042166900 src/Tools/isac/Build_Isac.thy
--- a/src/Tools/isac/Build_Isac.thy	Tue Apr 21 16:53:17 2020 +0200
+++ b/src/Tools/isac/Build_Isac.thy	Wed Apr 22 11:06:48 2020 +0200
@@ -150,11 +150,11 @@
   REPLACE BY Know_Store... (has been overlooked)
     calcelems.sml:val rew_ord' = Unsynchronized.ref ...
   KEEP FOR TRACING
-    calcelems.sml:val trace_rewrite = Unsynchronized.ref false;
-    calcelems.sml:val depth = Unsynchronized.ref 99999;
-    calcelems.sml:val lim_rewrite = Unsynchronized.ref 99999;
-    calcelems.sml:val lim_deriv = Unsynchronized.ref 100;
-    Interpret/script.sml:val trace_LI = Unsynchronized.ref false;
+    rewrite.sml:val Rewrite.trace_on = Unsynchronized.ref false;
+    rewrite.sml:val depth = Unsynchronized.ref 99999;
+    rewrite.sml:val lim_rewrite = Unsynchronized.ref 99999;
+    rewrite.sml:val lim_deriv = Unsynchronized.ref 100;
+    Interpret/rewtools.sml:val LItool.trace = Unsynchronized.ref false;
   KEEP FOR EASIER DEVELOPMENT
     calcelems.sml:val check_guhs_unique = Unsynchronized.ref true;
   KEEP FOR DEMOS