1.1 --- a/test/Tools/isac/ProgLang/rewrite.sml	Sat Feb 24 11:14:56 2018 +0100
     1.2 +++ b/test/Tools/isac/ProgLang/rewrite.sml	Sat Feb 24 16:09:24 2018 +0100
     1.3 @@ -11,8 +11,8 @@
     1.4  "table of contents --------------------------------------";
     1.5  "--------------------------------------------------------";
     1.6  "----------- assemble rewrite ---------------------------";
     1.7 -"----------- test rewriting without Isac's thys ---------";
     1.8 -"----------- conditional rewriting without Isac's thys --";
     1.9 +"----------- test rewriting without Isac session --------";
    1.10 +"----------- conditional rewriting without Isac session -";
    1.11  "----------- step through 'and rew_sub': ----------------";
    1.12  "----------- step through 'fun rewrite_terms_'  ---------";
    1.13  "----------- rewrite_inst_ bdvs -------------------------";
    1.14 @@ -304,7 +304,7 @@
    1.15  "===== example which raised the problem =================";
    1.16  val t = @{term "1 / EI * (L * q_0 * x / 2 + -1 * q_0 * x ^^^ 2 / 2)"};
    1.17  "----- rewrite_set_inst_ norm_Rational_noadd_fractions--";
    1.18 -val subs = [(str2term "bdv", str2term "x")];
    1.19 +val subs = [(@{term "bdv"}, @{term  "x"})];
    1.20  val rls = norm_Rational_noadd_fractions;
    1.21  val SOME (t', asms) = rewrite_set_inst_ thy true subs rls t;
    1.22  if term2str t' = "1 / EI * (L * q_0 * x / 2 + -1 * 1 * q_0 * x ^^^ 2 / 2)" andalso