1.1 --- a/test/Tools/isac/Knowledge/diff-app.sml Sun Oct 09 06:53:03 2022 +0200
1.2 +++ b/test/Tools/isac/Knowledge/diff-app.sml Sun Oct 09 07:44:22 2022 +0200
1.3 @@ -455,7 +455,7 @@
1.4 "--------------------- 30.4.03: maximum .. rewrite_set_ prog_expr ---------";
1.5 "--------------------- 30.4.03: maximum .. rewrite_set_ prog_expr ---------";
1.6 "--------------------- 30.4.03: maximum .. rewrite_set_ prog_expr ---------";
1.7 -TermC.str2term
1.8 +TermC.parse_test @{context}
1.9 "Program Maximum_value(f_ix::bool list)(m_m::real) (r_s::bool list)\
1.10 \ (v_v::real) (itv_v::real set) (err_r::bool) = \
1.11 \ (let e_e = (hd o (filterVar m_m)) r_s; \
1.12 @@ -470,22 +470,22 @@
1.13 \ [REAL mx_x, REAL (Rhs t_t), REAL v_v, REAL m_m, \
1.14 \ BOOL_LIST (dropWhile (ident e_e) r_s)])::bool list))";
1.15
1.16 -val f_ix = (TermC.str2term "f_ix::bool list",
1.17 - TermC.str2term "[r=Arbfix]");
1.18 -val m_m = (TermC.str2term "m_m::real",
1.19 - TermC.str2term "A");
1.20 -val r_s = (TermC.str2term "rs_s::bool list",
1.21 - TermC.str2term "[A = a*b, (a/2) \<up> 2 + (b/2) \<up> 2 = r \<up> 2]");
1.22 -val v_v = (TermC.str2term "v_v::real",
1.23 - TermC.str2term "b");
1.24 -val itv_v = (TermC.str2term "itv_v::real set",
1.25 - TermC.str2term "{x::real. 0 <= x & x <= 2*r}");
1.26 -val err_r = (TermC.str2term "err_r::bool",
1.27 - TermC.str2term "eps=0");
1.28 +val f_ix = (TermC.parse_test @{context} "f_ix::bool list",
1.29 + TermC.parse_test @{context} "[r=Arbfix]");
1.30 +val m_m = (TermC.parse_test @{context} "m_m::real",
1.31 + TermC.parse_test @{context} "A");
1.32 +val r_s = (TermC.parse_test @{context} "rs_s::bool list",
1.33 + TermC.parse_test @{context} "[A = a*b, (a/2) \<up> 2 + (b/2) \<up> 2 = r \<up> 2]");
1.34 +val v_v = (TermC.parse_test @{context} "v_v::real",
1.35 + TermC.parse_test @{context} "b");
1.36 +val itv_v = (TermC.parse_test @{context} "itv_v::real set",
1.37 + TermC.parse_test @{context} "{x::real. 0 <= x & x <= 2*r}");
1.38 +val err_r = (TermC.parse_test @{context} "err_r::bool",
1.39 + TermC.parse_test @{context} "eps=0");
1.40 val env = [f_ix, m_m, r_s ,v_v, itv_v, err_r];
1.41
1.42 (*--- 1.line in script ---*)
1.43 -val t = TermC.str2term "(hd o (filterVar m_m)) (r_s::bool list)";
1.44 +val t = TermC.parse_test @{context} "(hd o (filterVar m_m)) (r_s::bool list)";
1.45 val s = subst_atomic env t;
1.46 UnparseC.term s;
1.47 "(hd o filterVar A) [A = a * b, (a / 2) \<up> 2 + (b / 2) \<up> 2 = r \<up> 2]";
1.48 @@ -494,10 +494,10 @@
1.49 val s'' = UnparseC.term s';
1.50 if s''="A = a * b" then () else error "new behaviour with prog_expr 1.1.";
1.51 === inhibit exn 110726=============================================================*)
1.52 -val env = env @ [(TermC.str2term "e_e::bool",TermC.str2term "A = a * b")];
1.53 +val env = env @ [(TermC.parse_test @{context} "e_e::bool",TermC.parse_test @{context} "A = a * b")];
1.54
1.55 (*--- 2.line: condition alone ---*)
1.56 -val t = TermC.str2term "1 < length_h (r_s::bool list)";
1.57 +val t = TermC.parse_test @{context} "1 < length_h (r_s::bool list)";
1.58 val s = subst_atomic env t;
1.59 UnparseC.term s;
1.60 "1 < length_h [A = a * b, (a / 2) \<up> 2 + (b / 2) \<up> 2 = r \<up> 2]";
1.61 @@ -508,7 +508,7 @@
1.62 === inhibit exn 110726=============================================================*)
1.63
1.64 (*--- 2.line in script ---*)
1.65 -val t = TermC.str2term
1.66 +val t = TermC.parse_test @{context}
1.67 "(if 1 < length_h r_s \
1.68 \ then (SubProblem (Reals_s,[make,function],[no_met])\
1.69 \ [REAL m_m, REAL v_v, BOOL_LIST r_s])\
1.70 @@ -529,15 +529,15 @@
1.71 \ BOOL_LIST [A = a * b, (a / 2) \<up> 2 + (b / 2) \<up> 2 = r \<up> 2]]" then ()
1.72 else error "new behaviour with prog_expr 1.3.";
1.73 === inhibit exn 110726=============================================================*)
1.74 -val env = env @ [(TermC.str2term "t_t::bool",
1.75 - TermC.str2term "A = (2*sqrt(r \<up> 2-(b/2) \<up> 2)) * b")];
1.76 +val env = env @ [(TermC.parse_test @{context} "t_t::bool",
1.77 + TermC.parse_test @{context} "A = (2*sqrt(r \<up> 2-(b/2) \<up> 2)) * b")];
1.78
1.79
1.80
1.81 "---------------------- 1.5.03: Make_fun_by_explicit ---------------------";
1.82 "---------------------- 1.5.03: Make_fun_by_explicit ---------------------";
1.83 "---------------------- 1.5.03: Make_fun_by_explicit ---------------------";
1.84 -TermC.str2term
1.85 +TermC.parse_test @{context}
1.86 "Program Make_fun_by_explicit (f_f::real) (v_v::real) \
1.87 \ (eqs::bool list) = \
1.88 \ (let h_h = (hd o (filterVar f_f)) eqs; \
1.89 @@ -547,32 +547,32 @@
1.90 \ (s_1::bool list)=(SubProblem(Reals_s,[univar,equation],[no_met])\
1.91 \ [BOOL e_1, REAL v_1])\
1.92 \ in Substitute [(v_1 = (rhs o hd) s_1)] h_h)";
1.93 -val f_f = (TermC.str2term "f_f::real",
1.94 - TermC.str2term "A");
1.95 -val v_v = (TermC.str2term "v_v::real",
1.96 - TermC.str2term "b");
1.97 -val eqs=(TermC.str2term "eqs::bool list",
1.98 - TermC.str2term "[A = a * b, (a / 2) \<up> 2 + (b / 2) \<up> 2 = r \<up> 2]");
1.99 +val f_f = (TermC.parse_test @{context} "f_f::real",
1.100 + TermC.parse_test @{context} "A");
1.101 +val v_v = (TermC.parse_test @{context} "v_v::real",
1.102 + TermC.parse_test @{context} "b");
1.103 +val eqs=(TermC.parse_test @{context} "eqs::bool list",
1.104 + TermC.parse_test @{context} "[A = a * b, (a / 2) \<up> 2 + (b / 2) \<up> 2 = r \<up> 2]");
1.105 val env = [f_f, v_v, eqs];
1.106
1.107 (*--- 1.line in script ---*)
1.108 -val t = TermC.str2term "(hd o (filterVar v_v)) (eqs::bool list)";
1.109 +val t = TermC.parse_test @{context} "(hd o (filterVar v_v)) (eqs::bool list)";
1.110 val s = subst_atomic env t;
1.111 UnparseC.term s;
1.112 -val t = TermC.str2term
1.113 +val t = TermC.parse_test @{context}
1.114 "(hd o filterVar b) [A = a * b, (a / 2) \<up> 2 + (b / 2) \<up> 2 = r \<up> 2]";
1.115 val SOME (t',_) = rewrite_set_ ctxt false prog_expr t;
1.116 val s' = UnparseC.term t';
1.117 (*=== inhibit exn 110726=============================================================
1.118 if s' = "A = a * b" then () else error "new behaviour with prog_expr 2.1";
1.119 === inhibit exn 110726=============================================================*)
1.120 -val env = env @ [(TermC.str2term "h_h::bool", TermC.str2term s')];
1.121 +val env = env @ [(TermC.parse_test @{context} "h_h::bool", TermC.parse_test @{context} s')];
1.122
1.123 (*--- 2.line in script ---*)
1.124 -val t = TermC.str2term "hd (dropWhile (ident h_h) (eqs::bool list))";
1.125 +val t = TermC.parse_test @{context} "hd (dropWhile (ident h_h) (eqs::bool list))";
1.126 val s = subst_atomic env t;
1.127 UnparseC.term s;
1.128 -val t = TermC.str2term
1.129 +val t = TermC.parse_test @{context}
1.130 "hd (dropWhile (ident (A = a * b))\
1.131 \ [A = a * b, (a / 2) \<up> 2 + (b / 2) \<up> 2 = r \<up> 2])";
1.132 (*=== inhibit exn 110726=============================================================
1.133 @@ -583,47 +583,47 @@
1.134 if s' = "(a / 2) \<up> 2 + (b / 2) \<up> 2 = r \<up> 2" then ()
1.135 else error "new behaviour with prog_expr 2.2";
1.136 === inhibit exn 110726=============================================================*)
1.137 -val env = env @ [(TermC.str2term "e_1::bool", TermC.str2term s')];
1.138 +val env = env @ [(TermC.parse_test @{context} "e_1::bool", TermC.parse_test @{context} s')];
1.139
1.140 (*--- 3.line in script ---*)
1.141 -val t = TermC.str2term "dropWhile (ident f_f) (Vars (h_h::bool))";
1.142 +val t = TermC.parse_test @{context} "dropWhile (ident f_f) (Vars (h_h::bool))";
1.143 val s = subst_atomic env t;
1.144 UnparseC.term s;
1.145 -val t = TermC.str2term "dropWhile (ident A) (Vars (A = a * b))";
1.146 +val t = TermC.parse_test @{context} "dropWhile (ident A) (Vars (A = a * b))";
1.147 (*=== inhibit exn 110726=============================================================
1.148 val SOME (t',_) = rewrite_set_ thy false prog_expr t;
1.149 val s' = UnparseC.term t';
1.150 if s' = "[a, b]" then () else error "new behaviour with prog_expr 2.3";
1.151 === inhibit exn 110726=============================================================*)
1.152 -val env = env @ [(TermC.str2term "vs_s::real list", TermC.str2term s')];
1.153 +val env = env @ [(TermC.parse_test @{context} "vs_s::real list", TermC.parse_test @{context} s')];
1.154
1.155 (*--- 4.line in script ---*)
1.156 -val t = TermC.str2term "hd (dropWhile (ident v_v) v_s)";
1.157 +val t = TermC.parse_test @{context} "hd (dropWhile (ident v_v) v_s)";
1.158 val s = subst_atomic env t;
1.159 UnparseC.term s;
1.160 -val t = TermC.str2term "hd (dropWhile (ident b) [a, b])";
1.161 +val t = TermC.parse_test @{context} "hd (dropWhile (ident b) [a, b])";
1.162 (*=== inhibit exn 110726=============================================================
1.163 val SOME (t',_) = rewrite_set_ thy false prog_expr t;
1.164 val s' = UnparseC.term t';
1.165 if s' = "a" then () else error "new behaviour with prog_expr 2.4.";
1.166 === inhibit exn 110726=============================================================*)
1.167 -val env = env @ [(TermC.str2term "v_1::real", TermC.str2term s')];
1.168 +val env = env @ [(TermC.parse_test @{context} "v_1::real", TermC.parse_test @{context} s')];
1.169
1.170 (*--- 5.line in script ---*)
1.171 -val t = TermC.str2term "(SubProblem(Reals_s,[univar,equation],[no_met])\
1.172 +val t = TermC.parse_test @{context} "(SubProblem(Reals_s,[univar,equation],[no_met])\
1.173 \ [BOOL e_1, REAL v_1])";
1.174 val s = subst_atomic env t;
1.175 UnparseC.term s;
1.176 "SubProblem (Reals_s, [univar, equation], [no_met])\n\
1.177 \ [BOOL ((a / 2) \<up> 2 + (b / 2) \<up> 2 = r \<up> 2), REAL a]";
1.178 -val env = env @ [(TermC.str2term "s_1::bool list",
1.179 - TermC.str2term "[a = 2 * sqrt (r \<up> 2 - (b/2) \<up> 2)]")];
1.180 +val env = env @ [(TermC.parse_test @{context} "s_1::bool list",
1.181 + TermC.parse_test @{context} "[a = 2 * sqrt (r \<up> 2 - (b/2) \<up> 2)]")];
1.182
1.183 (*--- 6.line in script ---*)
1.184 -val t = TermC.str2term "Substitute [(v_1 = (rhs o hd) (s_1::bool list))] (h_h::bool)";
1.185 +val t = TermC.parse_test @{context} "Substitute [(v_1 = (rhs o hd) (s_1::bool list))] (h_h::bool)";
1.186 val s = subst_atomic env t;
1.187 UnparseC.term s;
1.188 -val t = TermC.str2term
1.189 +val t = TermC.parse_test @{context}
1.190 "Substitute [(a = (rhs o hd) [a = 2 * sqrt (r \<up> 2 - (b / 2) \<up> 2)])]\n\
1.191 \ (A = a * b)";
1.192 (*=== inhibit exn 110726=============================================================
1.193 @@ -638,7 +638,7 @@
1.194 "---------------------- 2.5.03: Make_fun_by_new_variable -----------------";
1.195 "---------------------- 2.5.03: Make_fun_by_new_variable -----------------";
1.196 "---------------------- 2.5.03: Make_fun_by_new_variable -----------------";
1.197 -TermC.str2term
1.198 +TermC.parse_test @{context}
1.199 "Program Make_fun_by_new_variable (f_f::real) (v_v::real) \
1.200 \ (eqs::bool list) = \
1.201 \(let h_h = (hd o (filterVar f_f)) eqs; \
1.202 @@ -653,32 +653,32 @@
1.203 \ (s_2::bool list) = (SubProblem (Reals_s,[univar,equation],[no_met])\
1.204 \ [BOOL e_2, REAL v_2])\
1.205 \in Substitute [(v_1 = (rhs o hd) s_1),(v_2 = (rhs o hd) s_2)] h_h)";
1.206 -val f_ = (TermC.str2term "f_f::real",
1.207 - TermC.str2term "A");
1.208 -val v_v = (TermC.str2term "v_v::real",
1.209 - TermC.str2term "alpha");
1.210 -val eqs=(TermC.str2term "eqs::bool list",
1.211 - TermC.str2term "[A=a*b, a/2=r*sin alpha, b/2=r*cos (alpha::real)]");
1.212 +val f_ = (TermC.parse_test @{context} "f_f::real",
1.213 + TermC.parse_test @{context} "A");
1.214 +val v_v = (TermC.parse_test @{context} "v_v::real",
1.215 + TermC.parse_test @{context} "alpha");
1.216 +val eqs=(TermC.parse_test @{context} "eqs::bool list",
1.217 + TermC.parse_test @{context} "[A=a*b, a/2=r*sin alpha, b/2=r*cos (alpha::real)]");
1.218 val env = [f_f, v_v, eqs];
1.219
1.220 (*--- 1.line in script ---*)
1.221 -val t = TermC.str2term "(hd o (filterVar (f_f::real))) (eqs::bool list)";
1.222 +val t = TermC.parse_test @{context} "(hd o (filterVar (f_f::real))) (eqs::bool list)";
1.223 val s = subst_atomic env t;
1.224 UnparseC.term s;
1.225 -val t = TermC.str2term
1.226 +val t = TermC.parse_test @{context}
1.227 "(hd o filterVar A) [A = a * b, a / 2 = r * sin alpha, b / 2 = r * cos alpha]";
1.228 val SOME (t',_) = rewrite_set_ ctxt false prog_expr t;
1.229 val s' = UnparseC.term t';
1.230 (*=== inhibit exn 110726=============================================================
1.231 if s' = "A = a * b" then() else error "new behaviour with prog_expr 3.1.";
1.232 -val env = env @ [(TermC.str2term "h_h::bool", TermC.str2term s')];
1.233 +val env = env @ [(TermC.parse_test @{context} "h_h::bool", TermC.parse_test @{context} s')];
1.234 === inhibit exn 110726=============================================================*)
1.235
1.236 (*--- 2.line in script ---*)
1.237 -val t = TermC.str2term "dropWhile (ident (h_h::bool)) (eqs::bool list)";
1.238 +val t = TermC.parse_test @{context} "dropWhile (ident (h_h::bool)) (eqs::bool list)";
1.239 val s = subst_atomic env t;
1.240 UnparseC.term s;
1.241 -val t = TermC.str2term
1.242 +val t = TermC.parse_test @{context}
1.243 "dropWhile (ident (A = a * b))\
1.244 \ [A = a * b, a / 2 = r * sin alpha, b / 2 = r * cos alpha]";
1.245 (*=== inhibit exn 110726=============================================================
1.246 @@ -687,49 +687,49 @@
1.247 if s' = "[a / 2 = r * sin alpha, b / 2 = r * cos alpha]"
1.248 then () else error "new behaviour with prog_expr 3.2.";
1.249 === inhibit exn 110726=============================================================*)
1.250 -val env = env @ [(TermC.str2term "es_s::bool list", TermC.str2term s')];
1.251 +val env = env @ [(TermC.parse_test @{context} "es_s::bool list", TermC.parse_test @{context} s')];
1.252
1.253 (*--- 3.line in script ---*)
1.254 -val t = TermC.str2term "dropWhile (ident (f_f::real)) (Vars (h_h::bool))";
1.255 +val t = TermC.parse_test @{context} "dropWhile (ident (f_f::real)) (Vars (h_h::bool))";
1.256 val s = subst_atomic env t;
1.257 UnparseC.term s;
1.258 -val t = TermC.str2term "dropWhile (ident A) (Vars (A = a * b))";
1.259 +val t = TermC.parse_test @{context} "dropWhile (ident A) (Vars (A = a * b))";
1.260 (*=== inhibit exn 110726=============================================================
1.261 val SOME (t',_) = rewrite_set_ thy false prog_expr t;
1.262 val s' = UnparseC.term t';
1.263 if s' = "[a, b]" then () else error "new behaviour with prog_expr 3.3.";
1.264 === inhibit exn 110726=============================================================*)
1.265 -val env = env @ [(TermC.str2term "vs_s::real list", TermC.str2term s')];
1.266 +val env = env @ [(TermC.parse_test @{context} "vs_s::real list", TermC.parse_test @{context} s')];
1.267
1.268 (*--- 4.line in script ---*)
1.269 -val t = TermC.str2term "nth_h 1 v_s";
1.270 +val t = TermC.parse_test @{context} "nth_h 1 v_s";
1.271 val s = subst_atomic env t;
1.272 UnparseC.term s;
1.273 -val t = TermC.str2term "nth_h 1 [a, b]";
1.274 +val t = TermC.parse_test @{context} "nth_h 1 [a, b]";
1.275 (*=== inhibit exn 110726=============================================================
1.276 val SOME (t',_) = rewrite_set_ thy false prog_expr t;
1.277 val s' = UnparseC.term t';
1.278 if s' = "a" then () else error "new behaviour with prog_expr 3.4.";
1.279 === inhibit exn 110726=============================================================*)
1.280 -val env = env @ [(TermC.str2term "v_1", TermC.str2term s')];
1.281 +val env = env @ [(TermC.parse_test @{context} "v_1", TermC.parse_test @{context} s')];
1.282
1.283 (*--- 5.line in script ---*)
1.284 -val t = TermC.str2term "nth_h 2 v_s";
1.285 +val t = TermC.parse_test @{context} "nth_h 2 v_s";
1.286 val s = subst_atomic env t;
1.287 UnparseC.term s;
1.288 -val t = TermC.str2term "nth_h 2 [a, b]";
1.289 +val t = TermC.parse_test @{context} "nth_h 2 [a, b]";
1.290 (*=== inhibit exn 110726=============================================================
1.291 val SOME (t',_) = rewrite_set_ thy false prog_expr t;
1.292 val s' = UnparseC.term t';
1.293 if s' = "b" then () else error "new behaviour with prog_expr 3.5.";
1.294 === inhibit exn 110726=============================================================*)
1.295 -val env = env @ [(TermC.str2term "v_2", TermC.str2term s')];
1.296 +val env = env @ [(TermC.parse_test @{context} "v_2", TermC.parse_test @{context} s')];
1.297
1.298 (*--- 6.line in script ---*)
1.299 -val t = TermC.str2term "(hd o (filterVar v_1)) (es_s::bool list)";
1.300 +val t = TermC.parse_test @{context} "(hd o (filterVar v_1)) (es_s::bool list)";
1.301 val s = subst_atomic env t;
1.302 UnparseC.term s;
1.303 -val t = TermC.str2term
1.304 +val t = TermC.parse_test @{context}
1.305 "(hd o filterVar a) [a / 2 = r * sin alpha, b / 2 = r * cos alpha]";
1.306 val SOME (t',_) = rewrite_set_ ctxt false prog_expr t;
1.307 val s' = UnparseC.term t';
1.308 @@ -737,14 +737,14 @@
1.309 if s' = "a / 2 = r * sin alpha" then ()
1.310 else error "new behaviour with prog_expr 3.6.";
1.311 === inhibit exn 110726=============================================================*)
1.312 -val e_1 = TermC.str2term "e_1::bool";
1.313 -val env = env @ [(e_1, TermC.str2term s')];
1.314 +val e_1 = TermC.parse_test @{context} "e_1::bool";
1.315 +val env = env @ [(e_1, TermC.parse_test @{context} s')];
1.316
1.317 (*--- 7.line in script ---*)
1.318 -val t = TermC.str2term "(hd o (filterVar v_2)) (es_s::bool list)";
1.319 +val t = TermC.parse_test @{context} "(hd o (filterVar v_2)) (es_s::bool list)";
1.320 val s = subst_atomic env t;
1.321 UnparseC.term s;
1.322 -val t = TermC.str2term
1.323 +val t = TermC.parse_test @{context}
1.324 "(hd o filterVar b) [a / 2 = r * sin alpha, b / 2 = r * cos alpha]";
1.325 val SOME (t',_) = rewrite_set_ ctxt false prog_expr t;
1.326 val s' = UnparseC.term t';
1.327 @@ -752,30 +752,30 @@
1.328 if s' = "b / 2 = r * cos alpha" then ()
1.329 else error "new behaviour with prog_expr 3.7.";
1.330 === inhibit exn 110726=============================================================*)
1.331 -val env = env @ [(TermC.str2term "e_2::bool", TermC.str2term s')];
1.332 +val env = env @ [(TermC.parse_test @{context} "e_2::bool", TermC.parse_test @{context} s')];
1.333
1.334 (*--- 8.line in script ---*)
1.335 -val t = TermC.str2term "(SubProblem (Reals_s,[univar,equation],[no_met])\
1.336 +val t = TermC.parse_test @{context} "(SubProblem (Reals_s,[univar,equation],[no_met])\
1.337 \ [BOOL e_1, REAL v_1])";
1.338 val s = subst_atomic env t;
1.339 UnparseC.term s;
1.340 "SubProblem (Reals_s, [univar, equation], [no_met])\
1.341 \ [BOOL (a / 2 = r * sin alpha), REAL a]";
1.342 -val s_1 = TermC.str2term "[a = 2*r*sin alpha]";
1.343 -val env = env @ [(TermC.str2term "s_1::bool list", s_1)];
1.344 +val s_1 = TermC.parse_test @{context} "[a = 2*r*sin alpha]";
1.345 +val env = env @ [(TermC.parse_test @{context} "s_1::bool list", s_1)];
1.346
1.347 (*--- 9.line in script ---*)
1.348 -val t = TermC.str2term "(SubProblem (Reals_s,[univar,equation],[no_met])\
1.349 +val t = TermC.parse_test @{context} "(SubProblem (Reals_s,[univar,equation],[no_met])\
1.350 \ [BOOL e_2, REAL v_2])";
1.351 val s = subst_atomic env t;
1.352 UnparseC.term s;
1.353 "SubProblem (Reals_s, [univar, equation], [no_met])\
1.354 \ [BOOL (b / 2 = r * cos alpha), REAL b]";
1.355 -val s_2 = TermC.str2term "[b = 2*r*cos alpha]";
1.356 -val env = env @ [(TermC.str2term "s_2::bool list", s_2)];
1.357 +val s_2 = TermC.parse_test @{context} "[b = 2*r*cos alpha]";
1.358 +val env = env @ [(TermC.parse_test @{context} "s_2::bool list", s_2)];
1.359
1.360 (*--- 10.line in script ---*)
1.361 -val t = TermC.str2term
1.362 +val t = TermC.parse_test @{context}
1.363 "Substitute [(v_1 = (rhs o hd) s_1),(v_2 = (rhs o hd) s_2)] (h_h::bool)";
1.364 val s = subst_atomic env t;
1.365 UnparseC.term s;