1.1 --- a/test/Tools/isac/MathEngBasic/rewrite.sml	Tue Apr 21 16:16:11 2020 +0200
     1.2 +++ b/test/Tools/isac/MathEngBasic/rewrite.sml	Tue Apr 21 16:53:17 2020 +0200
     1.3 @@ -246,8 +246,8 @@
     1.4  (writeln o UnparseC.term) t;
     1.5  if UnparseC.term t = "L * c_3 + c_4 = 0 + -1 * (-1 * (q_0 * L ^^^ 2) / 2)"
     1.6  then () else error "rewrite.sml rewrite_inst_ bdvs";
     1.7 -> trace_rewrite:=true;
     1.8 -trace_rewrite:=false;--------------------------------------------*)
     1.9 +> Trace.trace_rewrite:=true;
    1.10 +Trace.trace_rewrite:=false;--------------------------------------------*)
    1.11  
    1.12  
    1.13  "----------- check diff 2002--2009-3 --------------------";
    1.14 @@ -327,7 +327,7 @@
    1.15  writeln "----- rewrite_set_inst_ norm_Rational_noadd_fractions--";
    1.16  val (*NONE*) SOME (t', asm) = rewrite_set_inst_ thy true subs rls t;
    1.17  UnparseC.term t' = "a * x / (b * x ^^^ 2)"; (*rew. by thm outside test case*)
    1.18 -(*checked visually: trace_rewrite looks like above for 2009*)
    1.19 +(*checked visually: Trace.trace_rewrite looks like above for 2009*)
    1.20  
    1.21  writeln "----- rewrite_ rat_mult_poly_r--------------------------";
    1.22  val NONE (*SOME (t'', _)*) = rewrite_ thy dummy_ord erls true thm t;
    1.23 @@ -422,9 +422,9 @@
    1.24                            Const ("HOL.True", _))) => ()
    1.25    | _ => error "rewrite.sml diff. eval_is_multUnordered 2b";
    1.26  
    1.27 -tracing "----- begin rewrite x^^^2 * x ---"; trace_rewrite := false;
    1.28 +tracing "----- begin rewrite x^^^2 * x ---"; Trace.trace_rewrite := false;
    1.29  val SOME (t', _) = rewrite_set_ thy true order_mult_ t;
    1.30 -tracing "----- end rewrite x^^^2 * x ---"; trace_rewrite := false;
    1.31 +tracing "----- end rewrite x^^^2 * x ---"; Trace.trace_rewrite := false;
    1.32  if UnparseC.term t' = "x * x ^^^ 2" then ()
    1.33  else error "rewrite.sml Poly.is'_multUnordered doesn't work";
    1.34  
    1.35 @@ -655,7 +655,7 @@
    1.36  
    1.37             rewrite__set_ thy (i + 1) false bdv rls a (*of*);
    1.38  
    1.39 -(*+*)trace_rewrite := true;
    1.40 +(*+*)Trace.trace_rewrite := true;
    1.41  
    1.42          (*this was False; vvvv--- means: indeterminate*)
    1.43      val (* SOME (t, a') *)NONE = (*case*)
    1.44 @@ -676,7 +676,7 @@
    1.45   :                             
    1.46   ###  asms accepted: [x \<noteq> 0]   stored: []
    1.47   : *)
    1.48 -trace_rewrite := false;
    1.49 +Trace.trace_rewrite := false;
    1.50  ( *\------- outcomment this code: otherwise the re-definition could infect tests lateron ------/*)
    1.51  
    1.52