1.1 --- a/test/Tools/isac/MathEngBasic/mstools.sml	Mon Jul 19 18:39:02 2021 +0200
     1.2 +++ b/test/Tools/isac/MathEngBasic/mstools.sml	Tue Jul 20 14:37:56 2021 +0200
     1.3 @@ -56,20 +56,20 @@
     1.4  "solutions L"
     1.5  
     1.6  before 6.5.03:
     1.7 -> val t = (Thm.term_of o the o (TermC.parse thy)) "testdscforlist [#1]";
     1.8 +> val t = TermC.parseNEW'' thy "testdscforlist [#1]";
     1.9  > val (d,ts) = Input_Descript.split t;
    1.10  > Input_Descript.join thy (d,ts);
    1.11  val it = "testdscforlist [#1]" : cterm
    1.12  
    1.13 -> val t = (Thm.term_of o the o (TermC.parse thy)) "(A::real)";
    1.14 +> val t = TermC.parseNEW'' thy "(A::real)";
    1.15  > val (d,ts) = Input_Descript.split t;
    1.16  val d = Const ("empty", "empty") : term
    1.17  val ts = [Free ("A", "RealDef.real")] : term list
    1.18 -> val t = (Thm.term_of o the o (TermC.parse thy)) "[R=(R::real)]";
    1.19 +> val t = TermC.parseNEW'' thy "[R=(R::real)]";
    1.20  > val (d,ts) = Input_Descript.split t;
    1.21  val d = Const ("empty", "empty") : term
    1.22  val ts = [Const # $ Free # $ Free (#,#)] : term list
    1.23 -> val t = (Thm.term_of o the o (TermC.parse thy)) "[#1,#2]";
    1.24 +> val t = TermC.parseNEW'' thy "[#1,#2]";
    1.25  > val (d,ts) = Input_Descript.split t;
    1.26  val ts = [Free ("#1", "'a"),Free ("#2", "'a")] : NOT WANTED
    1.27  *)
    1.28 @@ -77,13 +77,13 @@
    1.29  "----------- type penv -------------------------------------------------------------------------";
    1.30  "----------- type penv -------------------------------------------------------------------------";
    1.31  (*
    1.32 -  val e_ = (Thm.term_of o the o (TermC.parse thy)) "e_::bool";
    1.33 -  val ev = (Thm.term_of o the o (TermC.parse thy)) "#4 + #3 * x \<up> #2 = #0";
    1.34 -  val v_ = (Thm.term_of o the o (TermC.parse thy)) "v_";
    1.35 -  val vv = (Thm.term_of o the o (TermC.parse thy)) "x";
    1.36 -  val r_ = (Thm.term_of o the o (TermC.parse thy)) "err_::bool";
    1.37 -  val rv1 = (Thm.term_of o the o (TermC.parse thy)) "#0";
    1.38 -  val rv2 = (Thm.term_of o the o (TermC.parse thy)) "eps";
    1.39 +  val e_ = TermC.parseNEW'' thy "e_::bool";
    1.40 +  val ev = TermC.parseNEW'' thy "#4 + #3 * x \<up> #2 = #0";
    1.41 +  val v_ = TermC.parseNEW'' thy "v_";
    1.42 +  val vv = TermC.parseNEW'' thy "x";
    1.43 +  val r_ = TermC.parseNEW'' thy "err_::bool";
    1.44 +  val rv1 = TermC.parseNEW'' thy "#0";
    1.45 +  val rv2 = TermC.parseNEW'' thy "eps";
    1.46  
    1.47    val penv = [(e_,[ev]),(v_,[vv]),(r_,[rv2,rv2])]:penv;
    1.48    map getval penv;
    1.49 @@ -108,7 +108,7 @@
    1.50  val t as t1 $ t2 = TermC.str2term "antiDerivativeName M_b";
    1.51  pbl_ids ctxt t1 t2;
    1.52  
    1.53 -  val t = (Thm.term_of o the o (TermC.parse thy)) "fixedValues [r=Arbfix]";
    1.54 +  val t = TermC.parseNEW'' thy "fixedValues [r=Arbfix]";
    1.55    val (d,argl) = strip_comb t;
    1.56    Input_Descript.is_a d;                      (*see Input_Descript.split*)
    1.57    dest_list (d,argl);