1.1 --- a/test/Tools/isac/ADDTESTS/course/phst11/T2_Rewriting.thy	Tue Apr 21 16:16:11 2020 +0200
     1.2 +++ b/test/Tools/isac/ADDTESTS/course/phst11/T2_Rewriting.thy	Tue Apr 21 16:53:17 2020 +0200
     1.3 @@ -55,7 +55,7 @@
     1.4  \<close>
     1.5  ML \<open>
     1.6  val SOME (t, _) = Rewrite.rewrite_set_ thy true make_polynomial t; UnparseC.term t;
     1.7 -Celem.trace_rewrite := false;
     1.8 +Celem.Trace.trace_rewrite := false;
     1.9  \<close>
    1.10  
    1.11  section \<open>Note on bound variables\<close>
    1.12 @@ -155,13 +155,13 @@
    1.13  val SOME (t, _) = Rewrite.rewrite_set_ thy true norm_Rational t2; UnparseC.term t;
    1.14  \<close>
    1.15  text \<open>The simplifiers are quite busy when finding the above results. you can
    1.16 -  watch them at work by setting the switch 'trace_rewrite:\<close>
    1.17 +  watch them at work by setting the switch 'Trace.trace_rewrite:\<close>
    1.18  ML \<open>
    1.19 -Celem.trace_rewrite := false;
    1.20 +Celem.Trace.trace_rewrite := false;
    1.21  tracing "+++begin++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++";
    1.22  val SOME (t, _) = Rewrite.rewrite_set_ thy true norm_Rational t2; UnparseC.term t;
    1.23  tracing "+++end++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++";
    1.24 -Celem.trace_rewrite := false;
    1.25 +Celem.Trace.trace_rewrite := false;
    1.26  \<close>
    1.27  text \<open>You see what happend when you click the checkbox <Tracing> on the bar
    1.28    separating this window from the Output-window.