1.1 --- a/test/Tools/isac/MathEngBasic/rewrite.sml	Tue Jul 20 14:37:56 2021 +0200
     1.2 +++ b/test/Tools/isac/MathEngBasic/rewrite.sml	Tue Jul 27 11:21:14 2021 +0200
     1.3 @@ -36,7 +36,7 @@
     1.4  val thy = @{theory Complex_Main};
     1.5  val ctxt = @{context};
     1.6  val thm = @{thm add.commute};
     1.7 -val t = TermC.parseNEW'' thy "((r + u) + t) + s";
     1.8 +val t = (Thm.term_of o the) (TermC.parse thy "((r + u) + t) + s");
     1.9  "----- from old: fun rewrite__";
    1.10  val bdv = [];
    1.11  val r = TermC.inst_bdv bdv (Eval.norm (Thm.prop_of thm));
    1.12 @@ -52,9 +52,6 @@
    1.13  writeln(Syntax.string_of_term ctxt LHS);
    1.14  writeln(Syntax.string_of_term ctxt t);
    1.15  
    1.16 -(*broken with "reduce the number of TermC.parse*-------exception MATCH---------------------\\
    1.17 -TOODOO ERROR exception MATCH raised (line 284 of "pattern.ML)
    1.18 -
    1.19  (Pattern.match thy (LHS, t) (Vartab.empty, Vartab.empty));
    1.20  val (rew, RHS) = (Envir.subst_term 
    1.21    (Pattern.match thy (LHS, t) (Vartab.empty, Vartab.empty)) rtm, rtm);
    1.22 @@ -79,7 +76,7 @@
    1.23  (*is displayed on top of <response> buffer...*)
    1.24  Pretty.writeln (Proof_Context.pretty_term_abbrev @{context} r');
    1.25  Pretty.writeln (Proof_Context.pretty_term_abbrev @{context} t');
    1.26 ---broken with "reduce the number of TermC.parse*------------------------------------------//( **)
    1.27 +(**)
    1.28  
    1.29  "----------- test rewriting without Isac's thys ------------------------------------------------";
    1.30  "----------- test rewriting without Isac's thys ------------------------------------------------";