diff -r 56654afad89f -r f1fdb213717b test/Tools/isac/Knowledge/polyminus.sml
--- a/test/Tools/isac/Knowledge/polyminus.sml	Thu May 14 16:58:33 2020 +0200
+++ b/test/Tools/isac/Knowledge/polyminus.sml	Fri May 15 11:46:43 2020 +0200
@@ -278,7 +278,7 @@
 	    ["simplification","for_polynomials","with_minus"]))];
 moveActiveRoot 1;
 autoCalculate 1 CompleteCalc;
-val ((pt,p),_) = get_calc 1; show_pt pt;
+val ((pt,p),_) = get_calc 1; Test_Tool.show_pt pt;
 if p = ([], Res) andalso 
    UnparseC.term (get_obj g_res pt (fst p)) = "3 - 2 * e + 2 * f + 2 * g"
 then () else error "polyminus.sml: Vereinfache (3 - 2 * e + 2 * f...";
@@ -291,7 +291,7 @@
 	    ["simplification","for_polynomials","with_minus"]))];
 moveActiveRoot 1;
 autoCalculate 1 CompleteCalc;
-val ((pt,p),_) = get_calc 1; show_pt pt;
+val ((pt,p),_) = get_calc 1; Test_Tool.show_pt pt;
 if p = ([], Res) andalso 
    UnparseC.term (get_obj g_res pt (fst p)) = "3 + 3 * r + 6 * s - 8 * t"
 then () else error "polyminus.sml: Vereinfache 140 d)";
@@ -304,7 +304,7 @@
 	    ["simplification","for_polynomials","with_minus"]))];
 moveActiveRoot 1;
 autoCalculate 1 CompleteCalc;
-val ((pt,p),_) = get_calc 1; show_pt pt;
+val ((pt,p),_) = get_calc 1; Test_Tool.show_pt pt;
 if p = ([], Res) andalso 
    UnparseC.term (get_obj g_res pt (fst p)) = "- (3 * f)"
 then () else error "polyminus.sml: Vereinfache 139 c)";
@@ -317,7 +317,7 @@
 	    ["simplification","for_polynomials","with_minus"]))];
 moveActiveRoot 1;
 autoCalculate 1 CompleteCalc;
-val ((pt,p),_) = get_calc 1; show_pt pt;
+val ((pt,p),_) = get_calc 1; Test_Tool.show_pt pt;
 if p = ([], Res) andalso 
    UnparseC.term (get_obj g_res pt (fst p)) = "-3 * u - v"
 then () else error "polyminus.sml: Vereinfache 139 b)";
@@ -330,7 +330,7 @@
 	    ["simplification","for_polynomials","with_minus"]))];
 moveActiveRoot 1;
 autoCalculate 1 CompleteCalc;
-val ((pt,p),_) = get_calc 1; show_pt pt;
+val ((pt,p),_) = get_calc 1; Test_Tool.show_pt pt;
 if p = ([], Res) andalso 
    UnparseC.term (get_obj g_res pt (fst p)) = "-4 * u + 2 * v"
 then () else error "polyminus.sml: Vereinfache 138 a)";
@@ -369,7 +369,7 @@
 val ((pt,p),_) = get_calc 1;
 if p = ([], Res) andalso UnparseC.term (get_obj g_res pt (fst p)) = "11 = 11"
 then () else error "polyminus.sml: Probe 11 = 11";
-show_pt pt;
+Test_Tool.show_pt pt;
 
 "----------- pbl klammer polynom vereinfachen p.34 ---------------";
 "----------- pbl klammer polynom vereinfachen p.34 ---------------";
@@ -385,7 +385,7 @@
 if p = ([], Res) andalso 
    UnparseC.term (get_obj g_res pt (fst p)) = "1 + 14 * u"
 then () else error "polyminus.sml: Vereinfache (2*u - 5 - (3 - ...";
-show_pt pt;
+Test_Tool.show_pt pt;
 
 "======= probe p.34 -----";
 reset_states ();
@@ -399,7 +399,7 @@
 val ((pt,p),_) = get_calc 1;
 if p = ([], Res) andalso UnparseC.term (get_obj g_res pt (fst p)) = "29 = 29"
 then () else error "polyminus.sml: Probe 29 = 29";
-show_pt pt;
+Test_Tool.show_pt pt;
 
 "----------- try fun applyTactics --------------------------------";
 "----------- try fun applyTactics --------------------------------";
@@ -413,12 +413,12 @@
 autoCalculate 1 CompleteCalcHead;
 autoCalculate 1 (Steps 1);
 autoCalculate 1 (Steps 1);
-val ((pt,p),_) = get_calc 1; show_pt pt;
+val ((pt,p),_) = get_calc 1; Test_Tool.show_pt pt;
 "----- 1 ^^^";
 fetchApplicableTactics 1 0 p;
 val appltacs = specific_from_prog pt p;
 applyTactic 1 p (hd appltacs) (*addiere_x_plus_minus*);
-val ((pt,p),_) = get_calc 1; show_pt pt;
+val ((pt,p),_) = get_calc 1; Test_Tool.show_pt pt;
 "----- 2 ^^^";
 (*Rewrite.trace_on := true; ..stopped Test_Isac.thy*)
 val erls = erls_ordne_alphabetisch;
@@ -439,25 +439,25 @@
 
 
 applyTactic 1 p (hd (specific_from_prog pt p)) (*tausche_minus*);
-val ((pt,p),_) = get_calc 1; show_pt pt;
+val ((pt,p),_) = get_calc 1; Test_Tool.show_pt pt;
 "----- 3 ^^^";
 applyTactic 1 p (hd (specific_from_prog pt p)) (**);
-val ((pt,p),_) = get_calc 1; show_pt pt;
+val ((pt,p),_) = get_calc 1; Test_Tool.show_pt pt;
 "----- 4 ^^^";
 applyTactic 1 p (hd (specific_from_prog pt p)) (**);
-val ((pt,p),_) = get_calc 1; show_pt pt;
+val ((pt,p),_) = get_calc 1; Test_Tool.show_pt pt;
 "----- 5 ^^^";
 applyTactic 1 p (hd (specific_from_prog pt p)) (**);
-val ((pt,p),_) = get_calc 1; show_pt pt;
+val ((pt,p),_) = get_calc 1; Test_Tool.show_pt pt;
 "----- 6 ^^^";
 
 (*<CALCMESSAGE> failure </CALCMESSAGE>
 applyTactic 1 p (hd (specific_from_prog pt p)) (**);
-val ((pt,p),_) = get_calc 1; show_pt pt;
+val ((pt,p),_) = get_calc 1; Test_Tool.show_pt pt;
 "----- 7 ^^^";
 *)
 autoCalculate 1 CompleteCalc;
-val ((pt,p),_) = get_calc 1; show_pt pt;
+val ((pt,p),_) = get_calc 1; Test_Tool.show_pt pt;
 (*independent from failure above: met_simp_poly_minus not confluent:
 (([9], Res), - (8 * g) + 10 * g + (3 - 2 * e + 2 * f)),
 (([], Res), - (8 * g) + 10 * g + (3 - 2 * e + 2 * f))]
@@ -472,7 +472,7 @@
 	    ["simplification","for_polynomials","with_minus"]))];
 moveActiveRoot 1;
 autoCalculate 1 CompleteCalc;
-val ((pt,p),_) = get_calc 1; show_pt pt;
+val ((pt,p),_) = get_calc 1; Test_Tool.show_pt pt;
 if p = ([], Res) andalso UnparseC.term (get_obj g_res pt (fst p)) = "2 * g + h"
 then () else error "polyminus.sml: addiere_vor_minus";
 
@@ -485,7 +485,7 @@
 	    ["simplification","for_polynomials","with_minus"]))];
 moveActiveRoot 1;
 autoCalculate 1 CompleteCalc;
-val ((pt,p),_) = get_calc 1; show_pt pt;
+val ((pt,p),_) = get_calc 1; Test_Tool.show_pt pt;
 if p = ([], Res) andalso UnparseC.term (get_obj g_res pt (fst p)) = "f + 2 * g"
 then () else error "polyminus.sml: tausche_vor_plus";
 
@@ -529,7 +529,7 @@
 	    ["simplification","for_polynomials","with_parentheses_mult"]))];
 moveActiveRoot 1;
 autoCalculate 1 CompleteCalc;
-val ((pt,p),_) = get_calc 1; show_pt pt;
+val ((pt,p),_) = get_calc 1; Test_Tool.show_pt pt;
 if p = ([], Res) andalso 
    UnparseC.term (get_obj g_res pt (fst p)) = "-2 + 12 * a ^^^ 2 + 5 * a"
 then () else error "polyminus.sml: Vereinfache (2*u - 5 - (3 - ...";
@@ -543,7 +543,7 @@
 	    ["simplification","for_polynomials","with_parentheses_mult"]))];
 moveActiveRoot 1;
 autoCalculate 1 CompleteCalc;
-val ((pt,p),_) = get_calc 1; show_pt pt;
+val ((pt,p),_) = get_calc 1; Test_Tool.show_pt pt;
 if p = ([], Res) andalso UnparseC.term (get_obj g_res pt (fst p)) = "12 * a - 16 * q" 
 then () else error "pbl binom polynom vereinfachen: cube";