1.1 --- a/test/Tools/isac/MathEngBasic/mstools.sml	Sun Oct 09 06:53:03 2022 +0200
     1.2 +++ b/test/Tools/isac/MathEngBasic/mstools.sml	Sun Oct 09 07:44:22 2022 +0200
     1.3 @@ -20,38 +20,38 @@
     1.4  "----------- fun Input_Descript.join -- fun Input_Descript.split -------------------------------";
     1.5  "----------- fun Input_Descript.join -- fun Input_Descript.split -------------------------------";
     1.6  "----------- fun Input_Descript.join -- fun Input_Descript.split -------------------------------";
     1.7 -(*val t = TermC.str2term "maximum A"; 
     1.8 +(*val t = TermC.parse_test @{context} "maximum A"; 
     1.9  > val (d,ts) = Input_Descript.split thy t; Input_Descript.join thy (d,ts);
    1.10  val it = "maximum A" : cterm
    1.11 -> val t = TermC.str2term "fixedValues [r=Arbfix]"; 
    1.12 +> val t = TermC.parse_test @{context} "fixedValues [r=Arbfix]"; 
    1.13  > val (d,ts) = Input_Descript.split thy t; Input_Descript.join thy (d,ts);
    1.14  "fixedValues [r = Arbfix]"
    1.15 -> val t = TermC.str2term "valuesFor [a]"; 
    1.16 +> val t = TermC.parse_test @{context} "valuesFor [a]"; 
    1.17  > val (d,ts) = Input_Descript.split thy t; Input_Descript.join thy (d,ts);
    1.18  "valuesFor [a]"
    1.19 -> val t = TermC.str2term "valuesFor [a,b]"; 
    1.20 +> val t = TermC.parse_test @{context} "valuesFor [a,b]"; 
    1.21  > val (d,ts) = Input_Descript.split thy t; Input_Descript.join thy (d,ts);
    1.22  "valuesFor [a, b]"
    1.23 -> val t = TermC.str2term "relations [A=a*b, (a/2) \<up> 2 + (b/2) \<up> 2 = r \<up> 2]"; 
    1.24 +> val t = TermC.parse_test @{context} "relations [A=a*b, (a/2) \<up> 2 + (b/2) \<up> 2 = r \<up> 2]"; 
    1.25  > val (d,ts) = Input_Descript.split thy t; Input_Descript.join thy (d,ts);
    1.26  relations [A = a * b, (a / 2) \<up> 2 + (b / 2) \<up> 2 = r \<up> 2]"
    1.27 -> val t = TermC.str2term "boundVariable a";
    1.28 +> val t = TermC.parse_test @{context} "boundVariable a";
    1.29  > val (d,ts) = Input_Descript.split thy t; Input_Descript.join thy (d,ts);
    1.30  "boundVariable a"
    1.31 -> val t = TermC.str2term "interval {x::real. 0 <= x & x <= 2*r}"; 
    1.32 +> val t = TermC.parse_test @{context} "interval {x::real. 0 <= x & x <= 2*r}"; 
    1.33  > val (d,ts) = Input_Descript.split thy t; Input_Descript.join thy (d,ts);
    1.34  "interval {x. 0 <= x & x <= 2 * r}"
    1.35  
    1.36 -> val t = TermC.str2term "equality (sqrt(9+4*x)=sqrt x + sqrt(5+x))"; 
    1.37 +> val t = TermC.parse_test @{context} "equality (sqrt(9+4*x)=sqrt x + sqrt(5+x))"; 
    1.38  > val (d,ts) = Input_Descript.split thy t; Input_Descript.join thy (d,ts);
    1.39  "equality (sqrt (9 + 4 * x) = sqrt x + sqrt (5 + x))"
    1.40 -> val t = TermC.str2term "solveFor x"; 
    1.41 +> val t = TermC.parse_test @{context} "solveFor x"; 
    1.42  > val (d,ts) = Input_Descript.split thy t; Input_Descript.join thy (d,ts);
    1.43  "solveFor x"
    1.44 -> val t = TermC.str2term "errorBound (eps=0)"; 
    1.45 +> val t = TermC.parse_test @{context} "errorBound (eps=0)"; 
    1.46  > val (d,ts) = Input_Descript.split thy t; Input_Descript.join thy (d,ts);
    1.47  "errorBound (eps = 0)"
    1.48 -> val t = TermC.str2term "solutions L";
    1.49 +> val t = TermC.parse_test @{context} "solutions L";
    1.50  > val (d,ts) = Input_Descript.split thy t; Input_Descript.join thy (d,ts);
    1.51  "solutions L"
    1.52  
    1.53 @@ -105,7 +105,7 @@
    1.54  "----------- fun pbl_ids -----------------------------------------------------------------------";
    1.55  "----------- fun pbl_ids -----------------------------------------------------------------------";
    1.56  (*
    1.57 -val t as t1 $ t2 = TermC.str2term "antiDerivativeName M_b";
    1.58 +val t as t1 $ t2 = TermC.parse_test @{context} "antiDerivativeName M_b";
    1.59  pbl_ids ctxt t1 t2;
    1.60  
    1.61    val t = (Thm.term_of o the o (TermC.parse thy)) "fixedValues [r=Arbfix]";