1.1 --- a/test/Tools/isac/MathEngBasic/rewrite.sml Tue Apr 21 16:53:17 2020 +0200
1.2 +++ b/test/Tools/isac/MathEngBasic/rewrite.sml Wed Apr 22 11:06:48 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.trace_rewrite:=true;
1.8 -Trace.trace_rewrite:=false;--------------------------------------------*)
1.9 +> Rewrite.trace_on:=true;
1.10 +Rewrite.trace_on:=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.trace_rewrite looks like above for 2009*)
1.19 +(*checked visually: Rewrite.trace_on 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.trace_rewrite := false;
1.28 +tracing "----- begin rewrite x^^^2 * x ---"; Rewrite.trace_on := false;
1.29 val SOME (t', _) = rewrite_set_ thy true order_mult_ t;
1.30 -tracing "----- end rewrite x^^^2 * x ---"; Trace.trace_rewrite := false;
1.31 +tracing "----- end rewrite x^^^2 * x ---"; Rewrite.trace_on := 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.trace_rewrite := true;
1.40 +(*+*)Rewrite.trace_on := 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.trace_rewrite := false;
1.49 +Rewrite.trace_on := false;
1.50 ( *\------- outcomment this code: otherwise the re-definition could infect tests lateron ------/*)
1.51
1.52