diff -r a3d65f3b495f -r 4e6fc3336336 test/Tools/isac/Knowledge/polyminus.sml
--- a/test/Tools/isac/Knowledge/polyminus.sml	Tue Apr 21 16:16:11 2020 +0200
+++ b/test/Tools/isac/Knowledge/polyminus.sml	Tue Apr 21 16:53:17 2020 +0200
@@ -66,13 +66,13 @@
 "----------- watch order_add_mult  -------------------------------";
 "----------- watch order_add_mult  -------------------------------";
 "----- with these simple variables it works...";
-(*trace_rewrite := true; ..stopped Test_Isac.thy*)
-trace_rewrite:=false;
+(*Trace.trace_rewrite := true; ..stopped Test_Isac.thy*)
+Trace.trace_rewrite:=false;
 val t = str2term "((a + d) + c) + b";
 val SOME (t,_) = rewrite_set_ thy false order_add_mult t; UnparseC.term t;
 if UnparseC.term t = "a + (b + (c + d))" then ()
 else error "polyminus.sml 1 watch order_add_mult";
-trace_rewrite:=false;
+Trace.trace_rewrite:=false;
 
 "----- the same stepwise...";
 val od = ord_make_polynomial true (@{theory "Poly"});
@@ -169,7 +169,7 @@
 val SOME (t,_) = rewrite_ thy od erls false @{thm real_num_collect} t; UnparseC.term t;
 
 "======= test rewrite_, rewrite_set_";
-(*trace_rewrite := true; ..stopped Test_Isac.thy*)
+(*Trace.trace_rewrite := true; ..stopped Test_Isac.thy*)
 val erls = erls_ordne_alphabetisch;
 val t = str2term "b + a";
 val SOME (t,_) = rewrite_set_ thy false ordne_alphabetisch t; UnparseC.term t;
@@ -227,8 +227,8 @@
 if UnparseC.term t = "3 - 2 * e + 2 * f + 2 * g" then ()
 else error "polyminus.sml: verschoenere 3 + -2 * e ...";
 
-(*trace_rewrite := true; ..stopped Test_Isac.thy*)
-trace_rewrite:=false;
+(*Trace.trace_rewrite := true; ..stopped Test_Isac.thy*)
+Trace.trace_rewrite:=false;
 
 "----------- met simplification for_polynomials with_minus -------";
 "----------- met simplification for_polynomials with_minus -------";
@@ -420,7 +420,7 @@
 applyTactic 1 p (hd appltacs) (*addiere_x_plus_minus*);
 val ((pt,p),_) = get_calc 1; show_pt pt;
 "----- 2 ^^^";
-(*trace_rewrite := true; ..stopped Test_Isac.thy*)
+(*Trace.trace_rewrite := true; ..stopped Test_Isac.thy*)
 val erls = erls_ordne_alphabetisch;
 val t = str2term "- 9 + 12 + 5 * e - 7 * e + (6 - 4) * f - 8 * g + 10 * g";
 val SOME (t',_) = 
@@ -435,7 +435,7 @@
 val SOME (t',_) = 
     rewrite_set_ (@{theory "Isac_Knowledge"}) false ordne_alphabetisch t;
 UnparseC.term t';     "- 9 + 12 + 5 * e - 7 * e - 8 * g + 10 * g + (- 4 + 6) * f";
-trace_rewrite := false;
+Trace.trace_rewrite := false;
 
 
 applyTactic 1 p (hd (specific_from_prog pt p)) (*tausche_minus*);
@@ -577,9 +577,9 @@
 	      (*"(~ True) = False"*)
 	      Thm ("not_false",ThmC.numerals_to_Free @{thm not_false})
 	      (*"(~ False) = True"*)];
-(*trace_rewrite := true; ..stopped Test_Isac.thy*)
+(*Trace.trace_rewrite := true; ..stopped Test_Isac.thy*)
 val SOME (t', _) = rewrite_set_ thy false prls t;
-trace_rewrite := false;
+Trace.trace_rewrite := false;
 
 "--- does the respective prls rewrite the whole predicate ?";
 val t = str2term 
@@ -587,9 +587,9 @@
 	    \     matchsub (?a * (?b - ?c)) (8 * (a - q) + a - 2 * q) | \
 	    \     matchsub ((?b + ?c) * ?a) (8 * (a - q) + a - 2 * q) | \
 	    \     matchsub ((?b - ?c) * ?a) (8 * (a - q) + a - 2 * q) )";
-(*trace_rewrite := true; ..stopped Test_Isac.thy*)
+(*Trace.trace_rewrite := true; ..stopped Test_Isac.thy*)
 val SOME (t', _) = rewrite_set_ thy false prls t;
-trace_rewrite := false;
+Trace.trace_rewrite := false;
 if UnparseC.term t' = "False" then ()
 else error "polyminus.sml Not (matchsub (?a * (?b + ?c)) (8 ...";