1.1 --- a/test/Tools/isac/Knowledge/polyminus.sml Fri Apr 10 16:16:09 2020 +0200
1.2 +++ b/test/Tools/isac/Knowledge/polyminus.sml Fri Apr 10 18:32:36 2020 +0200
1.3 @@ -69,8 +69,8 @@
1.4 (*trace_rewrite := true; ..stopped Test_Isac.thy*)
1.5 trace_rewrite:=false;
1.6 val t = str2term "((a + d) + c) + b";
1.7 -val SOME (t,_) = rewrite_set_ thy false order_add_mult t; UnparseC.term2str t;
1.8 -if UnparseC.term2str t = "a + (b + (c + d))" then ()
1.9 +val SOME (t,_) = rewrite_set_ thy false order_add_mult t; UnparseC.term t;
1.10 +if UnparseC.term t = "a + (b + (c + d))" then ()
1.11 else error "polyminus.sml 1 watch order_add_mult";
1.12 trace_rewrite:=false;
1.13
1.14 @@ -78,39 +78,39 @@
1.15 val od = ord_make_polynomial true (@{theory "Poly"});
1.16 val t = str2term "((a + d) + c) + b";
1.17 "((a + d) + c) + b";
1.18 -val SOME (t,_) = rewrite_ thy od Rule_Set.empty true @{thm add.commute} t; UnparseC.term2str t;
1.19 +val SOME (t,_) = rewrite_ thy od Rule_Set.empty true @{thm add.commute} t; UnparseC.term t;
1.20 "b + ((a + d) + c)";
1.21 -val SOME (t,_) = rewrite_ thy od Rule_Set.empty true @{thm add.commute} t; UnparseC.term2str t;
1.22 +val SOME (t,_) = rewrite_ thy od Rule_Set.empty true @{thm add.commute} t; UnparseC.term t;
1.23 "b + (c + (a + d))";
1.24 -val SOME (t,_) = rewrite_ thy od Rule_Set.empty true @{thm add.left_commute} t;UnparseC.term2str t;
1.25 +val SOME (t,_) = rewrite_ thy od Rule_Set.empty true @{thm add.left_commute} t;UnparseC.term t;
1.26 "b + (a + (c + d))";
1.27 -val SOME (t,_) = rewrite_ thy od Rule_Set.empty true @{thm add.left_commute} t;UnparseC.term2str t;
1.28 +val SOME (t,_) = rewrite_ thy od Rule_Set.empty true @{thm add.left_commute} t;UnparseC.term t;
1.29 "a + (b + (c + d))";
1.30 -if UnparseC.term2str t = "a + (b + (c + d))" then ()
1.31 +if UnparseC.term t = "a + (b + (c + d))" then ()
1.32 else error "polyminus.sml 2 watch order_add_mult";
1.33
1.34 "----- if parentheses are right, left_commute is (almost) sufficient...";
1.35 val t = str2term "a + (d + (c + b))";
1.36 "a + (d + (c + b))";
1.37 -val SOME (t,_) = rewrite_ thy od Rule_Set.empty true @{thm add.left_commute} t;UnparseC.term2str t;
1.38 +val SOME (t,_) = rewrite_ thy od Rule_Set.empty true @{thm add.left_commute} t;UnparseC.term t;
1.39 "a + (c + (d + b))";
1.40 -val SOME (t,_) = rewrite_ thy od Rule_Set.empty true @{thm add.commute} t;UnparseC.term2str t;
1.41 +val SOME (t,_) = rewrite_ thy od Rule_Set.empty true @{thm add.commute} t;UnparseC.term t;
1.42 "a + (c + (b + d))";
1.43 -val SOME (t,_) = rewrite_ thy od Rule_Set.empty true @{thm add.left_commute} t;UnparseC.term2str t;
1.44 +val SOME (t,_) = rewrite_ thy od Rule_Set.empty true @{thm add.left_commute} t;UnparseC.term t;
1.45 "a + (b + (c + d))";
1.46
1.47 "----- but we do not want the parentheses at right; thus: cond.rew.";
1.48 "WN0712707 complicated monomials do not yet work ...";
1.49 val t = str2term "((5*a + 4*d) + 3*c) + 2*b";
1.50 -val SOME (t,_) = rewrite_set_ thy false order_add_mult t; UnparseC.term2str t;
1.51 -if UnparseC.term2str t = "2 * b + (3 * c + (4 * d + 5 * a))" then ()
1.52 +val SOME (t,_) = rewrite_set_ thy false order_add_mult t; UnparseC.term t;
1.53 +if UnparseC.term t = "2 * b + (3 * c + (4 * d + 5 * a))" then ()
1.54 else error "polyminus.sml: order_add_mult changed";
1.55
1.56 "----- here we see rew_sub going into subterm with ord.rew....";
1.57 val od = ord_make_polynomial false (@{theory "Poly"});
1.58 val t = str2term "b + a + c + d";
1.59 -val SOME (t,_) = rewrite_ thy od Rule_Set.empty false @{thm add.commute} t; UnparseC.term2str t;
1.60 -val SOME (t,_) = rewrite_ thy od Rule_Set.empty false @{thm add.commute} t; UnparseC.term2str t;
1.61 +val SOME (t,_) = rewrite_ thy od Rule_Set.empty false @{thm add.commute} t; UnparseC.term t;
1.62 +val SOME (t,_) = rewrite_ thy od Rule_Set.empty false @{thm add.commute} t; UnparseC.term t;
1.63 (*@@@ rew_sub gosub: t = d + (b + a + c)
1.64 @@@ rew_sub begin: t = b + a + c*)
1.65
1.66 @@ -160,54 +160,54 @@
1.67
1.68 val erls = erls_ordne_alphabetisch;
1.69 val t = str2term "b + a";
1.70 -val SOME (t,_) = rewrite_ thy od erls false @{thm tausche_plus} t; UnparseC.term2str t;
1.71 -if UnparseC.term2str t = "a + b" then ()
1.72 +val SOME (t,_) = rewrite_ thy od erls false @{thm tausche_plus} t; UnparseC.term t;
1.73 +if UnparseC.term t = "a + b" then ()
1.74 else error "polyminus.sml: ordne_alphabetisch1 b + a";
1.75
1.76 val erls = Atools_erls;
1.77 val t = str2term "2*a + 3*a";
1.78 -val SOME (t,_) = rewrite_ thy od erls false @{thm real_num_collect} t; UnparseC.term2str t;
1.79 +val SOME (t,_) = rewrite_ thy od erls false @{thm real_num_collect} t; UnparseC.term t;
1.80
1.81 "======= test rewrite_, rewrite_set_";
1.82 (*trace_rewrite := true; ..stopped Test_Isac.thy*)
1.83 val erls = erls_ordne_alphabetisch;
1.84 val t = str2term "b + a";
1.85 -val SOME (t,_) = rewrite_set_ thy false ordne_alphabetisch t; UnparseC.term2str t;
1.86 -if UnparseC.term2str t = "a + b" then ()
1.87 +val SOME (t,_) = rewrite_set_ thy false ordne_alphabetisch t; UnparseC.term t;
1.88 +if UnparseC.term t = "a + b" then ()
1.89 else error "polyminus.sml: ordne_alphabetisch a + b";
1.90
1.91 val t = str2term "2*b + a";
1.92 -val SOME (t,_) = rewrite_set_ thy false ordne_alphabetisch t; UnparseC.term2str t;
1.93 -if UnparseC.term2str t = "a + 2 * b" then ()
1.94 +val SOME (t,_) = rewrite_set_ thy false ordne_alphabetisch t; UnparseC.term t;
1.95 +if UnparseC.term t = "a + 2 * b" then ()
1.96 else error "polyminus.sml: ordne_alphabetisch a + 2 * b";
1.97
1.98 val t = str2term "a + c + b";
1.99 -val SOME (t,_) = rewrite_set_ thy false ordne_alphabetisch t; UnparseC.term2str t;
1.100 -if UnparseC.term2str t = "a + b + c" then ()
1.101 +val SOME (t,_) = rewrite_set_ thy false ordne_alphabetisch t; UnparseC.term t;
1.102 +if UnparseC.term t = "a + b + c" then ()
1.103 else error "polyminus.sml: ordne_alphabetisch a + b + c";
1.104
1.105 "======= rewrite goes into subterms";
1.106 val t = str2term "a + c + b + d";
1.107 -val SOME (t,_) = rewrite_ thy od erls false @{thm tausche_plus_plus} t; UnparseC.term2str t;
1.108 -if UnparseC.term2str t = "a + b + c + d" then ()
1.109 +val SOME (t,_) = rewrite_ thy od erls false @{thm tausche_plus_plus} t; UnparseC.term t;
1.110 +if UnparseC.term t = "a + b + c + d" then ()
1.111 else error "polyminus.sml: ordne_alphabetisch1 a + b + c + d";
1.112
1.113 val t = str2term "a + c + d + b";
1.114 -val SOME (t,_) = rewrite_set_ thy false ordne_alphabetisch t; UnparseC.term2str t;
1.115 -if UnparseC.term2str t = "a + b + c + d" then ()
1.116 +val SOME (t,_) = rewrite_set_ thy false ordne_alphabetisch t; UnparseC.term t;
1.117 +if UnparseC.term t = "a + b + c + d" then ()
1.118 else error "polyminus.sml: ordne_alphabetisch2 a + b + c + d";
1.119
1.120 "======= here we see rew_sub going into subterm with cond.rew....";
1.121 val t = str2term "b + a + c + d";
1.122 -val SOME (t,_) = rewrite_ thy od erls false @{thm tausche_plus} t; UnparseC.term2str t;
1.123 -if UnparseC.term2str t = "a + b + c + d" then ()
1.124 +val SOME (t,_) = rewrite_ thy od erls false @{thm tausche_plus} t; UnparseC.term t;
1.125 +if UnparseC.term t = "a + b + c + d" then ()
1.126 else error "polyminus.sml: ordne_alphabetisch3 a + b + c + d";
1.127
1.128 "======= compile rls for the most complicated terms";
1.129 val t = str2term "5*e + 6*f - 8*g - 9 - 7*e - 4*f + 10*g + 12";
1.130 "5 * e + 6 * f - 8 * g - 9 - 7 * e - 4 * f + 10 * g + 12";
1.131 val SOME (t,_) = rewrite_set_ thy false ordne_alphabetisch t;
1.132 -if UnparseC.term2str t = "- 9 + 12 + 5 * e - 7 * e + 6 * f - 4 * f - 8 * g + 10 * g"
1.133 +if UnparseC.term t = "- 9 + 12 + 5 * e - 7 * e + 6 * f - 4 * f - 8 * g + 10 * g"
1.134 then () else error "polyminus.sml: ordne_alphabetisch finished";
1.135
1.136
1.137 @@ -216,7 +216,7 @@
1.138 "----------- build fasse_zusammen --------------------------------";
1.139 val t = str2term "- 9 + 12 + 5 * e - 7 * e + 6 * f - 4 * f - 8 * g + 10 * g";
1.140 val SOME (t,_) = rewrite_set_ thy false fasse_zusammen t;
1.141 -if UnparseC.term2str t = "3 + -2 * e + 2 * f + 2 * g" then ()
1.142 +if UnparseC.term t = "3 + -2 * e + 2 * f + 2 * g" then ()
1.143 else error "polyminus.sml: fasse_zusammen finished";
1.144
1.145 "----------- build verschoenere ----------------------------------";
1.146 @@ -224,7 +224,7 @@
1.147 "----------- build verschoenere ----------------------------------";
1.148 val t = str2term "3 + -2 * e + 2 * f + 2 * g";
1.149 val SOME (t,_) = rewrite_set_ thy false verschoenere t;
1.150 -if UnparseC.term2str t = "3 - 2 * e + 2 * f + 2 * g" then ()
1.151 +if UnparseC.term t = "3 - 2 * e + 2 * f + 2 * g" then ()
1.152 else error "polyminus.sml: verschoenere 3 + -2 * e ...";
1.153
1.154 (*trace_rewrite := true; ..stopped Test_Isac.thy*)
1.155 @@ -280,7 +280,7 @@
1.156 autoCalculate 1 CompleteCalc;
1.157 val ((pt,p),_) = get_calc 1; show_pt pt;
1.158 if p = ([], Res) andalso
1.159 - UnparseC.term2str (get_obj g_res pt (fst p)) = "3 - 2 * e + 2 * f + 2 * g"
1.160 + UnparseC.term (get_obj g_res pt (fst p)) = "3 - 2 * e + 2 * f + 2 * g"
1.161 then () else error "polyminus.sml: Vereinfache (3 - 2 * e + 2 * f...";
1.162
1.163 "======= 140 d ---";
1.164 @@ -293,7 +293,7 @@
1.165 autoCalculate 1 CompleteCalc;
1.166 val ((pt,p),_) = get_calc 1; show_pt pt;
1.167 if p = ([], Res) andalso
1.168 - UnparseC.term2str (get_obj g_res pt (fst p)) = "3 + 3 * r + 6 * s - 8 * t"
1.169 + UnparseC.term (get_obj g_res pt (fst p)) = "3 + 3 * r + 6 * s - 8 * t"
1.170 then () else error "polyminus.sml: Vereinfache 140 d)";
1.171
1.172 "======= 139 c ---";
1.173 @@ -306,7 +306,7 @@
1.174 autoCalculate 1 CompleteCalc;
1.175 val ((pt,p),_) = get_calc 1; show_pt pt;
1.176 if p = ([], Res) andalso
1.177 - UnparseC.term2str (get_obj g_res pt (fst p)) = "- (3 * f)"
1.178 + UnparseC.term (get_obj g_res pt (fst p)) = "- (3 * f)"
1.179 then () else error "polyminus.sml: Vereinfache 139 c)";
1.180
1.181 "======= 139 b ---";
1.182 @@ -319,7 +319,7 @@
1.183 autoCalculate 1 CompleteCalc;
1.184 val ((pt,p),_) = get_calc 1; show_pt pt;
1.185 if p = ([], Res) andalso
1.186 - UnparseC.term2str (get_obj g_res pt (fst p)) = "-3 * u - v"
1.187 + UnparseC.term (get_obj g_res pt (fst p)) = "-3 * u - v"
1.188 then () else error "polyminus.sml: Vereinfache 139 b)";
1.189
1.190 "======= 138 a ---";
1.191 @@ -332,7 +332,7 @@
1.192 autoCalculate 1 CompleteCalc;
1.193 val ((pt,p),_) = get_calc 1; show_pt pt;
1.194 if p = ([], Res) andalso
1.195 - UnparseC.term2str (get_obj g_res pt (fst p)) = "-4 * u + 2 * v"
1.196 + UnparseC.term (get_obj g_res pt (fst p)) = "-4 * u + 2 * v"
1.197 then () else error "polyminus.sml: Vereinfache 138 a)";
1.198
1.199 "----------- met probe fuer_polynom ------------------------------";
1.200 @@ -363,11 +363,11 @@
1.201 (* autoCalculate 1 CompleteCalcHead;
1.202 autoCalculate 1 (Steps 1);
1.203 autoCalculate 1 (Steps 1);
1.204 - val ((pt,p),_) = get_calc 1; UnparseC.term2str (get_obj g_res pt (fst p));
1.205 + val ((pt,p),_) = get_calc 1; UnparseC.term (get_obj g_res pt (fst p));
1.206 @@@@@WN081114 gives "??.empty", all "Pruefe" are the same,
1.207 although analogies work in interface.sml: FIXME.WN081114 in "Pruefe"*)
1.208 val ((pt,p),_) = get_calc 1;
1.209 -if p = ([], Res) andalso UnparseC.term2str (get_obj g_res pt (fst p)) = "11 = 11"
1.210 +if p = ([], Res) andalso UnparseC.term (get_obj g_res pt (fst p)) = "11 = 11"
1.211 then () else error "polyminus.sml: Probe 11 = 11";
1.212 show_pt pt;
1.213
1.214 @@ -383,7 +383,7 @@
1.215 autoCalculate 1 CompleteCalc;
1.216 val ((pt,p),_) = get_calc 1;
1.217 if p = ([], Res) andalso
1.218 - UnparseC.term2str (get_obj g_res pt (fst p)) = "1 + 14 * u"
1.219 + UnparseC.term (get_obj g_res pt (fst p)) = "1 + 14 * u"
1.220 then () else error "polyminus.sml: Vereinfache (2*u - 5 - (3 - ...";
1.221 show_pt pt;
1.222
1.223 @@ -397,7 +397,7 @@
1.224 moveActiveRoot 1;
1.225 autoCalculate 1 CompleteCalc;
1.226 val ((pt,p),_) = get_calc 1;
1.227 -if p = ([], Res) andalso UnparseC.term2str (get_obj g_res pt (fst p)) = "29 = 29"
1.228 +if p = ([], Res) andalso UnparseC.term (get_obj g_res pt (fst p)) = "29 = 29"
1.229 then () else error "polyminus.sml: Probe 29 = 29";
1.230 show_pt pt;
1.231
1.232 @@ -425,7 +425,7 @@
1.233 val t = str2term "- 9 + 12 + 5 * e - 7 * e + (6 - 4) * f - 8 * g + 10 * g";
1.234 val SOME (t',_) =
1.235 rewrite_ (@{theory "Isac_Knowledge"}) e_rew_ord erls false @{thm tausche_minus} t;
1.236 -UnparseC.term2str t'; "- 9 + 12 + 5 * e - 7 * e + (- 4 + 6) * f - 8 * g + 10 * g";
1.237 +UnparseC.term t'; "- 9 + 12 + 5 * e - 7 * e + (- 4 + 6) * f - 8 * g + 10 * g";
1.238
1.239 val t = str2term "- 9 + 12 + 5 * e - 7 * e + (6 - 4) * f - 8 * g + 10 * g";
1.240 val NONE =
1.241 @@ -434,7 +434,7 @@
1.242 val t = str2term "- 9 + 12 + 5 * e - 7 * e + (6 - 4) * f - 8 * g + 10 * g";
1.243 val SOME (t',_) =
1.244 rewrite_set_ (@{theory "Isac_Knowledge"}) false ordne_alphabetisch t;
1.245 -UnparseC.term2str t'; "- 9 + 12 + 5 * e - 7 * e - 8 * g + 10 * g + (- 4 + 6) * f";
1.246 +UnparseC.term t'; "- 9 + 12 + 5 * e - 7 * e - 8 * g + 10 * g + (- 4 + 6) * f";
1.247 trace_rewrite := false;
1.248
1.249
1.250 @@ -473,7 +473,7 @@
1.251 moveActiveRoot 1;
1.252 autoCalculate 1 CompleteCalc;
1.253 val ((pt,p),_) = get_calc 1; show_pt pt;
1.254 -if p = ([], Res) andalso UnparseC.term2str (get_obj g_res pt (fst p)) = "2 * g + h"
1.255 +if p = ([], Res) andalso UnparseC.term (get_obj g_res pt (fst p)) = "2 * g + h"
1.256 then () else error "polyminus.sml: addiere_vor_minus";
1.257
1.258
1.259 @@ -486,7 +486,7 @@
1.260 moveActiveRoot 1;
1.261 autoCalculate 1 CompleteCalc;
1.262 val ((pt,p),_) = get_calc 1; show_pt pt;
1.263 -if p = ([], Res) andalso UnparseC.term2str (get_obj g_res pt (fst p)) = "f + 2 * g"
1.264 +if p = ([], Res) andalso UnparseC.term (get_obj g_res pt (fst p)) = "f + 2 * g"
1.265 then () else error "polyminus.sml: tausche_vor_plus";
1.266
1.267 "----------- pbl binom polynom vereinfachen p.39 -----------------";
1.268 @@ -494,31 +494,31 @@
1.269 "----------- pbl binom polynom vereinfachen p.39 -----------------";
1.270 val rls = klammern_ausmultiplizieren;
1.271 val t = str2term "(3 * a + 2) * (4 * a - 1)";
1.272 -val SOME (t,_) = rewrite_set_ thy false rls t; UnparseC.term2str t;
1.273 +val SOME (t,_) = rewrite_set_ thy false rls t; UnparseC.term t;
1.274 "3 * a * (4 * a) - 3 * a * 1 + (2 * (4 * a) - 2 * 1)";
1.275 val rls = discard_parentheses;
1.276 -val SOME (t,_) = rewrite_set_ thy false rls t; UnparseC.term2str t;
1.277 +val SOME (t,_) = rewrite_set_ thy false rls t; UnparseC.term t;
1.278 "3 * a * 4 * a - 3 * a * 1 + (2 * 4 * a - 2 * 1)";
1.279 val rls = ordne_monome;
1.280 -val SOME (t,_) = rewrite_set_ thy false rls t; UnparseC.term2str t;
1.281 +val SOME (t,_) = rewrite_set_ thy false rls t; UnparseC.term t;
1.282 "3 * 4 * a * a - 1 * 3 * a + (2 * 4 * a - 1 * 2)";
1.283 (*
1.284 val t = str2term "3 * a * 4 * a";
1.285 val rls = ordne_monome;
1.286 -val SOME (t,_) = rewrite_set_ thy false rls t; UnparseC.term2str t;
1.287 +val SOME (t,_) = rewrite_set_ thy false rls t; UnparseC.term t;
1.288 *)
1.289 val rls = klammern_aufloesen;
1.290 -val SOME (t,_) = rewrite_set_ thy false rls t; UnparseC.term2str t;
1.291 +val SOME (t,_) = rewrite_set_ thy false rls t; UnparseC.term t;
1.292 "3 * 4 * a * a - 1 * 3 * a + 2 * 4 * a - 1 * 2";
1.293 val rls = ordne_alphabetisch;
1.294 (*TODO: make is_monom more general, a*a=a^2, ...*)
1.295 -val SOME (t,_) = rewrite_set_ thy false rls t; UnparseC.term2str t;
1.296 +val SOME (t,_) = rewrite_set_ thy false rls t; UnparseC.term t;
1.297 "3 * 4 * a * a - 1 * 2 - 1 * 3 * a + 2 * 4 * a";
1.298 (*STOPPED.WN080104
1.299 val rls = fasse_zusammen;
1.300 -val SOME (t,_) = rewrite_set_ thy false rls t; UnparseC.term2str t;
1.301 +val SOME (t,_) = rewrite_set_ thy false rls t; UnparseC.term t;
1.302 val rls = verschoenere;
1.303 -val SOME (t,_) = rewrite_set_ thy false rls t; UnparseC.term2str t;
1.304 +val SOME (t,_) = rewrite_set_ thy false rls t; UnparseC.term t;
1.305 *)
1.306
1.307 (*@@@@@@@*)
1.308 @@ -531,7 +531,7 @@
1.309 autoCalculate 1 CompleteCalc;
1.310 val ((pt,p),_) = get_calc 1; show_pt pt;
1.311 if p = ([], Res) andalso
1.312 - UnparseC.term2str (get_obj g_res pt (fst p)) = "-2 + 12 * a ^^^ 2 + 5 * a"
1.313 + UnparseC.term (get_obj g_res pt (fst p)) = "-2 + 12 * a ^^^ 2 + 5 * a"
1.314 then () else error "polyminus.sml: Vereinfache (2*u - 5 - (3 - ...";
1.315
1.316 "----------- pbl binom polynom vereinfachen: cube ----------------";
1.317 @@ -544,7 +544,7 @@
1.318 moveActiveRoot 1;
1.319 autoCalculate 1 CompleteCalc;
1.320 val ((pt,p),_) = get_calc 1; show_pt pt;
1.321 -if p = ([], Res) andalso UnparseC.term2str (get_obj g_res pt (fst p)) = "12 * a - 16 * q"
1.322 +if p = ([], Res) andalso UnparseC.term (get_obj g_res pt (fst p)) = "12 * a - 16 * q"
1.323 then () else error "pbl binom polynom vereinfachen: cube";
1.324
1.325 "----------- refine Vereinfache ----------------------------------";
1.326 @@ -590,7 +590,7 @@
1.327 (*trace_rewrite := true; ..stopped Test_Isac.thy*)
1.328 val SOME (t', _) = rewrite_set_ thy false prls t;
1.329 trace_rewrite := false;
1.330 -if UnparseC.term2str t' = "False" then ()
1.331 +if UnparseC.term t' = "False" then ()
1.332 else error "polyminus.sml Not (matchsub (?a * (?b + ?c)) (8 ...";
1.333
1.334 "----------- *** prep_pbt: syntax error in '#Where' of [v";
1.335 @@ -603,10 +603,10 @@
1.336 " matchsub (?a - (?b + ?c)) t_t | " ^
1.337 " matchsub (?a + (?b - ?c)) t_t )");
1.338 (*show_types := true;
1.339 -if UnparseC.term2str t = "~ (matchsub ((?a::real) + ((?b::real) + (?c::real))) (t_t::real) |\n matchsub (?a + (?b - ?c)) t_t |\n matchsub (?a - (?b + ?c)) t_t | matchsub (?a + (?b - ?c)) t_t)"
1.340 +if UnparseC.term t = "~ (matchsub ((?a::real) + ((?b::real) + (?c::real))) (t_t::real) |\n matchsub (?a + (?b - ?c)) t_t |\n matchsub (?a - (?b + ?c)) t_t | matchsub (?a + (?b - ?c)) t_t)"
1.341 then () else error "polyminus.sml type-structure of \"?a :: real\" changed 1";
1.342 show_types := false;*)
1.343 -if UnparseC.term2str t =
1.344 +if UnparseC.term t =
1.345 "\<not> (matchsub (?a + (?b + ?c)) t_t \<or>\n " ^
1.346 "matchsub (?a + (?b - ?c)) t_t \<or>\n " ^
1.347 "matchsub (?a - (?b + ?c)) t_t \<or> " ^