1.1 --- a/test/Tools/isac/Knowledge/diff.sml	Sun Oct 09 06:53:03 2022 +0200
     1.2 +++ b/test/Tools/isac/Knowledge/diff.sml	Sun Oct 09 07:44:22 2022 +0200
     1.3 @@ -218,11 +218,11 @@
     1.4  "----------- primed id ----------------------------------";
     1.5  "----------- primed id ----------------------------------";
     1.6  val ctxt = Proof_Context.init_global @{theory Isac_Knowledge};
     1.7 -val f_ = TermC.str2term "f_f::bool";
     1.8 -val f  = TermC.str2term "A = s * (a - s)";
     1.9 -val v_ = TermC.str2term "v_v";
    1.10 -val v  = TermC.str2term "s";
    1.11 -val screxp0 = TermC.str2term "Take ((primed (lhs f_f)) = d_d v_v (rhs f_f))";
    1.12 +val f_ = TermC.parse_test @{context} "f_f::bool";
    1.13 +val f  = TermC.parse_test @{context} "A = s * (a - s)";
    1.14 +val v_ = TermC.parse_test @{context} "v_v";
    1.15 +val v  = TermC.parse_test @{context} "s";
    1.16 +val screxp0 = TermC.parse_test @{context} "Take ((primed (lhs f_f)) = d_d v_v (rhs f_f))";
    1.17  TermC.atomty screxp0;
    1.18  
    1.19  val screxp1 = subst_atomic [(f_, f), (v_, v)] screxp0;
    1.20 @@ -268,32 +268,32 @@
    1.21  "----------- diff_conv, sym_diff_conv -------------------";
    1.22  "----------- diff_conv, sym_diff_conv -------------------";
    1.23  "----------- diff_conv, sym_diff_conv -------------------";
    1.24 -val subs = [(TermC.str2term "bdv", TermC.str2term "x")];
    1.25 +val subs = [(TermC.parse_test @{context} "bdv", TermC.parse_test @{context} "x")];
    1.26  val rls = diff_conv;
    1.27  
    1.28 -val t = TermC.str2term "2/x \<up> 2"; 
    1.29 +val t = TermC.parse_test @{context} "2/x \<up> 2"; 
    1.30  val SOME (t,_) = rewrite_set_inst_ ctxt false subs rls t; UnparseC.term t;
    1.31  if UnparseC.term t = "2 * x \<up> - 2" then () else error "diff.sml 1/x";
    1.32  
    1.33 -val t = TermC.str2term "sqrt (x \<up> 3)";
    1.34 +val t = TermC.parse_test @{context} "sqrt (x \<up> 3)";
    1.35  val SOME (t,_) = rewrite_set_inst_ ctxt false subs rls t; UnparseC.term t;
    1.36  if UnparseC.term t = "x \<up> (3 / 2)" then () else error "diff.sml x \<up> 1/2";
    1.37  
    1.38 -val t = TermC.str2term "2 / sqrt x \<up> 3";
    1.39 +val t = TermC.parse_test @{context} "2 / sqrt x \<up> 3";
    1.40  val SOME (t,_) = rewrite_set_inst_ ctxt false subs rls t; UnparseC.term t;
    1.41  if UnparseC.term t = "2 * x \<up> (- 3 / 2)" then () else error "diff.sml x \<up> - 1/2";
    1.42  
    1.43  val rls = diff_sym_conv;
    1.44  
    1.45 -val t = TermC.str2term "2 * x \<up> - 2";
    1.46 +val t = TermC.parse_test @{context} "2 * x \<up> - 2";
    1.47  val SOME (t, _) = rewrite_set_inst_ ctxt false subs rls t; UnparseC.term t;
    1.48  if UnparseC.term t = "2 / x \<up> 2" then () else error "diff.sml sym 1/x";
    1.49  
    1.50 -val t = TermC.str2term "x \<up> (3 / 2)";
    1.51 +val t = TermC.parse_test @{context} "x \<up> (3 / 2)";
    1.52  val SOME (t,_) = rewrite_set_inst_ ctxt false subs rls t; UnparseC.term t;
    1.53  if UnparseC.term t = "sqrt (x \<up> 3)" then ((*..wrong rewrite*)) else error"diff.sml sym x \<up> 1/x";
    1.54  
    1.55 -val t = TermC.str2term "2 * x \<up> (-3 / 2)";
    1.56 +val t = TermC.parse_test @{context} "2 * x \<up> (-3 / 2)";
    1.57  val SOME (t,_) = rewrite_set_inst_ ctxt false subs rls t; UnparseC.term t;
    1.58  if UnparseC.term t ="2 / sqrt (x \<up> 3)"then()else error"diff.sml sym x \<up> - 1/x";
    1.59  
    1.60 @@ -388,14 +388,14 @@
    1.61  "----------- tests for examples -------------------------";
    1.62  "----------- tests for examples -------------------------";
    1.63  "----- TermC.parse errors";
    1.64 -(*TermC.str2term "F  =  sqrt( y \<up> 2 - O) * (z + O \<up> 2)";
    1.65 -TermC.str2term "O";
    1.66 -TermC.str2term "OO"; ---errors*)
    1.67 -TermC.str2term "OOO";
    1.68 +(*TermC.parse_test @{context} "F  =  sqrt( y \<up> 2 - O) * (z + O \<up> 2)";
    1.69 +TermC.parse_test @{context} "O";
    1.70 +TermC.parse_test @{context} "OO"; ---errors*)
    1.71 +TermC.parse_test @{context} "OOO";
    1.72  
    1.73  "----- thm 'diff_prod_const'";
    1.74 -val subs = [(TermC.str2term "bdv", TermC.str2term "l")];
    1.75 -val f = TermC.str2term "G' = d_d l (l * sqrt (7 * s \<up> 2 - l \<up> 2))";
    1.76 +val subs = [(TermC.parse_test @{context} "bdv", TermC.parse_test @{context} "l")];
    1.77 +val f = TermC.parse_test @{context} "G' = d_d l (l * sqrt (7 * s \<up> 2 - l \<up> 2))";
    1.78  
    1.79  "------------inform for x \<up> 2+x+1 -------------------------";
    1.80  "------------inform for x \<up> 2+x+1 -------------------------";