diff -r 4fb7bbdaa1ac -r 4ac966aaa785 test/Tools/isac/MathEngBasic/rewrite.sml
--- a/test/Tools/isac/MathEngBasic/rewrite.sml	Tue Jun 21 13:51:04 2022 +0200
+++ b/test/Tools/isac/MathEngBasic/rewrite.sml	Tue Jun 21 16:04:43 2022 +0200
@@ -175,7 +175,7 @@
 "~~~~~ fun rewrite_ , args:"; val (thy, rew_ord, erls, bool, thm, term) =
   (thy, dummy_ord, erls, false, thm, tm);
 "~~~~~ fun rewrite__ , args:"; val (thy, i, bdv, tless, rls, put_asm, thm, ct) =
-  (thy, 1, []: (term * term) list, rew_ord, erls, bool, thm, term);
+  (thy, 1, []: Subst.T, rew_ord, erls, bool, thm, term);
 
 (**) val (t', asms, _(*lrd*), rew) = rew_sub thy i bdv tless rls put_asm ([(*root of the term*)]: TermC.path)
 		  (TermC.inst_bdv bdv (Eval.norm (Thm.prop_of thm))) ct;
@@ -466,7 +466,7 @@
 else error "rewrite.sml: diff. is_multUnordered, asms";
 val (thy, i, asms, bdv, rls) = 
     (thy, (i+1), [TermC.str2term "(x \<up> 2 * x) is_multUnordered"], 
-     [] : (term * term) list, erls);
+     [] : Subst.T, erls);
 case eval__true thy i asms bdv rls of 
     ([], true) => ()
   | _ => error "rewrite.sml: diff. is_multUnordered, eval__true";
@@ -496,7 +496,7 @@
 "~~~~~ fun rewrite_set_ , args:"; val (thy, bool, rls, term) = (thy, true, rls, t);
            rewrite__set_ thy 1 bool [] rls term;
 "~~~~~ and rewrite__set_ , args:"; val (thy, i, put_asm, bdv, rls, ct)
-  = (thy, 1, bool, []:(term * term) list, rls, term);
+  = (thy, 1, bool, []:Subst.T, rls, term);
 
 (*/------- outcomment this code: otherwise the re-definition could infect tests lateron ------\ * )
       datatype switch = Applicable.Yes | Noap;
@@ -691,6 +691,6 @@
 
 "~~~~~ fun rewrite_set_ , args:"; val (thy, bool, rls, term) = (thy, false, rls, term);
 "~~~~~ and rewrite__set_ , args:"; val (thy, i, put_asm, bdv, rls, ct) =
-  (thy, 1, bool, []: (term * term) list, rls, term);
+  (thy, 1, bool, []: Subst.T, rls, term);
 (*deleted after error detection*)