1.1 --- a/test/Tools/isac/Knowledge/rootrateq.sml	Sun Oct 09 06:53:03 2022 +0200
     1.2 +++ b/test/Tools/isac/Knowledge/rootrateq.sml	Sun Oct 09 07:44:22 2022 +0200
     1.3 @@ -114,8 +114,8 @@
     1.4    "check_elementwise: no set 1 = 2 + - 2 * sqrt x"*)
     1.5  
     1.6  (*---- 2nd try: we investigate the script ["RootEq", "solve_sq_root_equation"] found via pbl*)
     1.7 -val t = TermC.str2term "((lhs e_e) is_sqrtTerm_in v_v) | ((rhs e_e) is_sqrtTerm_in v_v)";
     1.8 -val t = TermC.str2term ("((lhs (1 = 2 * (1 + - 1 * sqrt x))) is_sqrtTerm_in x) |" ^
     1.9 +val t = TermC.parse_test @{context} "((lhs e_e) is_sqrtTerm_in v_v) | ((rhs e_e) is_sqrtTerm_in v_v)";
    1.10 +val t = TermC.parse_test @{context} ("((lhs (1 = 2 * (1 + - 1 * sqrt x))) is_sqrtTerm_in x) |" ^
    1.11                   " ((rhs (1 = 2 * (1 + - 1 * sqrt x))) is_sqrtTerm_in x)");
    1.12  val SOME (t, _) = rewrite_set_ thy true rooteq_srls t;
    1.13  UnparseC.term t = "True | True"; (*...was same in 2002 (NOT "True"); so program seems to take