1.1 --- a/test/Tools/isac/MathEngBasic/rewrite.sml	Tue Jun 21 13:51:04 2022 +0200
     1.2 +++ b/test/Tools/isac/MathEngBasic/rewrite.sml	Tue Jun 21 16:04:43 2022 +0200
     1.3 @@ -175,7 +175,7 @@
     1.4  "~~~~~ fun rewrite_ , args:"; val (thy, rew_ord, erls, bool, thm, term) =
     1.5    (thy, dummy_ord, erls, false, thm, tm);
     1.6  "~~~~~ fun rewrite__ , args:"; val (thy, i, bdv, tless, rls, put_asm, thm, ct) =
     1.7 -  (thy, 1, []: (term * term) list, rew_ord, erls, bool, thm, term);
     1.8 +  (thy, 1, []: Subst.T, rew_ord, erls, bool, thm, term);
     1.9  
    1.10  (**) val (t', asms, _(*lrd*), rew) = rew_sub thy i bdv tless rls put_asm ([(*root of the term*)]: TermC.path)
    1.11  		  (TermC.inst_bdv bdv (Eval.norm (Thm.prop_of thm))) ct;
    1.12 @@ -466,7 +466,7 @@
    1.13  else error "rewrite.sml: diff. is_multUnordered, asms";
    1.14  val (thy, i, asms, bdv, rls) = 
    1.15      (thy, (i+1), [TermC.str2term "(x \<up> 2 * x) is_multUnordered"], 
    1.16 -     [] : (term * term) list, erls);
    1.17 +     [] : Subst.T, erls);
    1.18  case eval__true thy i asms bdv rls of 
    1.19      ([], true) => ()
    1.20    | _ => error "rewrite.sml: diff. is_multUnordered, eval__true";
    1.21 @@ -496,7 +496,7 @@
    1.22  "~~~~~ fun rewrite_set_ , args:"; val (thy, bool, rls, term) = (thy, true, rls, t);
    1.23             rewrite__set_ thy 1 bool [] rls term;
    1.24  "~~~~~ and rewrite__set_ , args:"; val (thy, i, put_asm, bdv, rls, ct)
    1.25 -  = (thy, 1, bool, []:(term * term) list, rls, term);
    1.26 +  = (thy, 1, bool, []:Subst.T, rls, term);
    1.27  
    1.28  (*/------- outcomment this code: otherwise the re-definition could infect tests lateron ------\ * )
    1.29        datatype switch = Applicable.Yes | Noap;
    1.30 @@ -691,6 +691,6 @@
    1.31  
    1.32  "~~~~~ fun rewrite_set_ , args:"; val (thy, bool, rls, term) = (thy, false, rls, term);
    1.33  "~~~~~ and rewrite__set_ , args:"; val (thy, i, put_asm, bdv, rls, ct) =
    1.34 -  (thy, 1, bool, []: (term * term) list, rls, term);
    1.35 +  (thy, 1, bool, []: Subst.T, rls, term);
    1.36  (*deleted after error detection*)
    1.37