1.1 --- a/test/Tools/isac/Knowledge/polyeq-1.sml	Mon Apr 13 13:27:55 2020 +0200
     1.2 +++ b/test/Tools/isac/Knowledge/polyeq-1.sml	Mon Apr 13 15:31:23 2020 +0200
     1.3 @@ -299,7 +299,7 @@
     1.4  val fmz = ["equality (1 = (0::real))", "solveFor x", "solutions L"];
     1.5  val (dI',pI',mI') = ("PolyEq",["degree_0","polynomial","univariate","equation"],
     1.6                       ["PolyEq","solve_d0_polyeq_equation"]);
     1.7 -(*=== inhibit exn WN110914: declare_constraints doesnt work with num_str ========
     1.8 +(*=== inhibit exn WN110914: declare_constraints doesnt work with ThmC.numerals_to_Free ========
     1.9  TODO: change to "equality (x + -1*x = (0::real))"
    1.10        and search for an appropriate problem and method.
    1.11  
    1.12 @@ -964,27 +964,27 @@
    1.13  val SOME (t,asm) = rewrite_set_inst_ thy true inst rls t;
    1.14  UnparseC.term t = "-8 + (2 / 2 - x) ^^^ 2 = (2 / 2) ^^^ 2";
    1.15  
    1.16 -val thm = num_str @{thm square_explicit1};
    1.17 +val thm = ThmC.numerals_to_Free @{thm square_explicit1};
    1.18  val SOME (t,asm) = rewrite_ thy dummy_ord Rule_Set.Empty true thm t;
    1.19  UnparseC.term t = "(2 / 2 - x) ^^^ 2 = (2 / 2) ^^^ 2 - -8";
    1.20  
    1.21 -val thm = num_str @{thm root_plus_minus};
    1.22 +val thm = ThmC.numerals_to_Free @{thm root_plus_minus};
    1.23  val SOME (t,asm) = rewrite_ thy dummy_ord PolyEq_erls true thm t;
    1.24  UnparseC.term t = "2 / 2 - x = sqrt ((2 / 2) ^^^ 2 - -8) |"^
    1.25             "\n2 / 2 - x = -1 * sqrt ((2 / 2) ^^^ 2 - -8)";
    1.26  
    1.27  (*the thm bdv_explicit2* here required to be constrained to ::real*)
    1.28 -val thm = num_str @{thm bdv_explicit2};
    1.29 +val thm = ThmC.numerals_to_Free @{thm bdv_explicit2};
    1.30  val SOME (t,asm) = rewrite_inst_ thy dummy_ord Rule_Set.Empty true inst thm t;
    1.31  UnparseC.term t = "2 / 2 - x = sqrt ((2 / 2) ^^^ 2 - -8) |"^
    1.32                "\n-1 * x = - (2 / 2) + -1 * sqrt ((2 / 2) ^^^ 2 - -8)";
    1.33  
    1.34 -val thm = num_str @{thm bdv_explicit3};
    1.35 +val thm = ThmC.numerals_to_Free @{thm bdv_explicit3};
    1.36  val SOME (t,asm) = rewrite_inst_ thy dummy_ord Rule_Set.Empty true inst thm t;
    1.37  UnparseC.term t = "2 / 2 - x = sqrt ((2 / 2) ^^^ 2 - -8) |"^
    1.38                     "\nx = -1 * (- (2 / 2) + -1 * sqrt ((2 / 2) ^^^ 2 - -8))";
    1.39  
    1.40 -val thm = num_str @{thm bdv_explicit2};
    1.41 +val thm = ThmC.numerals_to_Free @{thm bdv_explicit2};
    1.42  val SOME (t,asm) = rewrite_inst_ thy dummy_ord Rule_Set.Empty true inst thm t;
    1.43  UnparseC.term t = "-1 * x = - (2 / 2) + sqrt ((2 / 2) ^^^ 2 - -8) |"^
    1.44                  "\nx = -1 * (- (2 / 2) + -1 * sqrt ((2 / 2) ^^^ 2 - -8))";