1.1 --- a/test/Tools/isac/ProgLang/rewrite.sml	Mon Apr 20 14:18:40 2015 +0200
     1.2 +++ b/test/Tools/isac/ProgLang/rewrite.sml	Mon Apr 20 16:02:09 2015 +0200
     1.3 @@ -35,7 +35,7 @@
     1.4  
     1.5  val thy = @{theory Complex_Main};
     1.6  val ctxt = @{context};
     1.7 -val thm = @{thm add_commute};
     1.8 +val thm = @{thm add.commute};
     1.9  val t = (term_of o the) (parse thy "((r + u) + t) + s");
    1.10  "----- from old: fun rewrite__";
    1.11  val bdv = [];
    1.12 @@ -85,7 +85,7 @@
    1.13  "===== rewriting with Isabelle2009-1 only, i.e without isac-hacks";
    1.14  val thy = @{theory Complex_Main};
    1.15  val ctxt = @{context};
    1.16 -val thm =  @{thm add_commute};
    1.17 +val thm =  @{thm add.commute};
    1.18  val tm = @{term "x + y*z::real"};
    1.19  
    1.20  val SOME (r,_) = (rewrite_ thy dummy_ord e_rls false thm tm)
    1.21 @@ -303,7 +303,10 @@
    1.22  "----- rewrite_set_inst_ norm_Rational_noadd_fractions--";
    1.23  val subs = [(str2term "bdv", str2term "x")];
    1.24  val rls = norm_Rational_noadd_fractions;
    1.25 -val NONE (*SOME (t', _)*) = rewrite_set_inst_ thy true subs rls t;
    1.26 +val SOME (t', asms) = rewrite_set_inst_ thy true subs rls t;
    1.27 +if term2str t' = "1 / EI * (L * q_0 * x / 2 + -1 * 1 * q_0 * x ^^^ 2 / 2)" andalso
    1.28 +  terms2str asms = "[]" then {}
    1.29 +else error "this was NONE with Isabelle2013-2 ?!?"
    1.30  "----- rewrite_ rat_mult_poly_r--------------------------";
    1.31  val thm = @{thm rat_mult_poly_r};
    1.32           "?c::real is_polyexp ==> (?a::real) / (?b::real) * ?c = ?a * ?c / ?b";