1.1 --- a/test/Tools/isac/Knowledge/polyeq-1.sml	Sun Oct 09 06:53:03 2022 +0200
     1.2 +++ b/test/Tools/isac/Knowledge/polyeq-1.sml	Sun Oct 09 07:44:22 2022 +0200
     1.3 @@ -323,16 +323,16 @@
     1.4  
     1.5  (** )end;( *local*)
     1.6  
     1.7 -val subs = [(TermC.str2term "bdv::real", TermC.str2term "x::real")];
     1.8 +val subs = [(TermC.parse_test @{context} "bdv::real", TermC.parse_test @{context} "x::real")];
     1.9  if ord_make_polynomial_in false(*true*) @{theory} subs (t1, t2) then ()  else error "still GREATER?";
    1.10  
    1.11 -val x = TermC.str2term "x ::real";
    1.12 +val x = TermC.parse_test @{context} "x ::real";
    1.13  
    1.14 -val t1 = TermC.numerals_to_Free (TermC.str2term "L * q_0 * x \<up> 2 / 4 ::real");
    1.15 +val t1 = TermC.numerals_to_Free (TermC.parse_test @{context} "L * q_0 * x \<up> 2 / 4 ::real");
    1.16  if 2006 = size_of_term' 1 false(*true*) x t1 
    1.17  then () else error "size_of_term' (L * q_0 * x \<up> 2) CHANGED)";
    1.18  
    1.19 -val t2 = TermC.numerals_to_Free (TermC.str2term "- 1 * (q_0 * x \<up> 3) :: real");
    1.20 +val t2 = TermC.numerals_to_Free (TermC.parse_test @{context} "- 1 * (q_0 * x \<up> 3) :: real");
    1.21  if 3004 = size_of_term' 1 false(*true*) x t2
    1.22  then () else error "size_of_term' (- 1 * (q_0 * x \<up> 3)) CHANGED";
    1.23