1.1 --- a/test/Tools/isac/ProgLang/rewrite.sml Tue Sep 28 08:58:06 2010 +0200
1.2 +++ b/test/Tools/isac/ProgLang/rewrite.sml Tue Sep 28 09:06:56 2010 +0200
1.3 @@ -203,21 +203,21 @@
1.4 val SOME (t', _) = rewrite_terms_ thy dummy_ord Erls equs t;
1.5 writeln "----------- rewrite_terms_ 1---------------------------";
1.6 if term2str t' = "M_b 0 = -1 * q_0 * 0 ^^^ 2 / 2 + 0 * c + c_2" then ()
1.7 -else raise error "rewrite.sml rewrite_terms_ [x = 0]";
1.8 +else error "rewrite.sml rewrite_terms_ [x = 0]";
1.9
1.10 val equs = [str2term "M_b 0 = 0"];
1.11 val t = str2term "M_b 0 = -1 * q_0 * 0 ^^^ 2 / 2 + 0 * c + c_2";
1.12 val SOME (t', _) = rewrite_terms_ thy dummy_ord Erls equs t;
1.13 writeln "----------- rewrite_terms_ 2---------------------------";
1.14 if term2str t' = "0 = -1 * q_0 * 0 ^^^ 2 / 2 + 0 * c + c_2" then ()
1.15 -else raise error "rewrite.sml rewrite_terms_ [M_b 0 = 0]";
1.16 +else error "rewrite.sml rewrite_terms_ [M_b 0 = 0]";
1.17
1.18 val equs = [str2term "x = 0", str2term"M_b 0 = 0"];
1.19 val t = str2term "M_b x = -1 * q_0 * x ^^^ 2 / 2 + x * c + c_2";
1.20 val SOME (t', _) = rewrite_terms_ thy dummy_ord Erls equs t;
1.21 writeln "----------- rewrite_terms_ 3---------------------------";
1.22 if term2str t' = "0 = -1 * q_0 * 0 ^^^ 2 / 2 + 0 * c + c_2" then ()
1.23 -else raise error "rewrite.sml rewrite_terms_ [x = 0, M_b 0 = 0]";
1.24 +else error "rewrite.sml rewrite_terms_ [x = 0, M_b 0 = 0]";
1.25
1.26
1.27 "----------- rewrite_inst_ bdvs -------------------------";
1.28 @@ -240,7 +240,7 @@
1.29 false bdvs (num_str @{separate_bdvs_add) t;
1.30 (writeln o term2str) t;
1.31 if term2str t = "L * c_3 + c_4 = 0 + -1 * (-1 * (q_0 * L ^^^ 2) / 2)"
1.32 -then () else raise error "rewrite.sml rewrite_inst_ bdvs";
1.33 +then () else error "rewrite.sml rewrite_inst_ bdvs";
1.34 trace_rewrite:=true;
1.35 trace_rewrite:=false;--------------------------------------------*)
1.36