diff -r 0042fe0bc764 -r 82428ca0d23e test/Tools/isac/Knowledge/polyeq-1.sml
--- a/test/Tools/isac/Knowledge/polyeq-1.sml	Mon Apr 13 13:27:55 2020 +0200
+++ b/test/Tools/isac/Knowledge/polyeq-1.sml	Mon Apr 13 15:31:23 2020 +0200
@@ -299,7 +299,7 @@
 val fmz = ["equality (1 = (0::real))", "solveFor x", "solutions L"];
 val (dI',pI',mI') = ("PolyEq",["degree_0","polynomial","univariate","equation"],
                      ["PolyEq","solve_d0_polyeq_equation"]);
-(*=== inhibit exn WN110914: declare_constraints doesnt work with num_str ========
+(*=== inhibit exn WN110914: declare_constraints doesnt work with ThmC.numerals_to_Free ========
 TODO: change to "equality (x + -1*x = (0::real))"
       and search for an appropriate problem and method.
 
@@ -964,27 +964,27 @@
 val SOME (t,asm) = rewrite_set_inst_ thy true inst rls t;
 UnparseC.term t = "-8 + (2 / 2 - x) ^^^ 2 = (2 / 2) ^^^ 2";
 
-val thm = num_str @{thm square_explicit1};
+val thm = ThmC.numerals_to_Free @{thm square_explicit1};
 val SOME (t,asm) = rewrite_ thy dummy_ord Rule_Set.Empty true thm t;
 UnparseC.term t = "(2 / 2 - x) ^^^ 2 = (2 / 2) ^^^ 2 - -8";
 
-val thm = num_str @{thm root_plus_minus};
+val thm = ThmC.numerals_to_Free @{thm root_plus_minus};
 val SOME (t,asm) = rewrite_ thy dummy_ord PolyEq_erls true thm t;
 UnparseC.term t = "2 / 2 - x = sqrt ((2 / 2) ^^^ 2 - -8) |"^
            "\n2 / 2 - x = -1 * sqrt ((2 / 2) ^^^ 2 - -8)";
 
 (*the thm bdv_explicit2* here required to be constrained to ::real*)
-val thm = num_str @{thm bdv_explicit2};
+val thm = ThmC.numerals_to_Free @{thm bdv_explicit2};
 val SOME (t,asm) = rewrite_inst_ thy dummy_ord Rule_Set.Empty true inst thm t;
 UnparseC.term t = "2 / 2 - x = sqrt ((2 / 2) ^^^ 2 - -8) |"^
               "\n-1 * x = - (2 / 2) + -1 * sqrt ((2 / 2) ^^^ 2 - -8)";
 
-val thm = num_str @{thm bdv_explicit3};
+val thm = ThmC.numerals_to_Free @{thm bdv_explicit3};
 val SOME (t,asm) = rewrite_inst_ thy dummy_ord Rule_Set.Empty true inst thm t;
 UnparseC.term t = "2 / 2 - x = sqrt ((2 / 2) ^^^ 2 - -8) |"^
                    "\nx = -1 * (- (2 / 2) + -1 * sqrt ((2 / 2) ^^^ 2 - -8))";
 
-val thm = num_str @{thm bdv_explicit2};
+val thm = ThmC.numerals_to_Free @{thm bdv_explicit2};
 val SOME (t,asm) = rewrite_inst_ thy dummy_ord Rule_Set.Empty true inst thm t;
 UnparseC.term t = "-1 * x = - (2 / 2) + sqrt ((2 / 2) ^^^ 2 - -8) |"^
                 "\nx = -1 * (- (2 / 2) + -1 * sqrt ((2 / 2) ^^^ 2 - -8))";