1.1 --- a/test/Tools/isac/ProgLang/evaluate.sml	Mon Jul 19 18:39:02 2021 +0200
     1.2 +++ b/test/Tools/isac/ProgLang/evaluate.sml	Tue Jul 20 14:37:56 2021 +0200
     1.3 @@ -129,13 +129,13 @@
     1.4  
     1.5  (*--------------(2): does divide work in Test_simplify ?: ------*)
     1.6   val thy = @{theory Test};
     1.7 - val t = (Thm.term_of o the o (TermC.parse thy)) "6 / 2";
     1.8 + val t = TermC.parseNEW'' thy "6 / 2";
     1.9   val rls = Test_simplify;
    1.10   val (t,_) = the (rewrite_set_ thy false rls t);
    1.11  (*val t = Free ("3", "Real.real") : term*)
    1.12  
    1.13  (*--------------(3): is_const works ?: -------------------------------------*)
    1.14 - val t = (Thm.term_of o the o (TermC.parse @{theory Test})) "2 is_const";
    1.15 + val t = TermC.parseNEW'' thy "2 is_const";
    1.16   TermC.atomty t;
    1.17   rewrite_set_ @{theory Test} false tval_rls t;
    1.18  (*val it = SOME (Const (\<^const_name>\<open>True\<close>, "bool"),[]) ... works*)
    1.19 @@ -152,19 +152,19 @@
    1.20   Rewrite.trace_on := false; (*true false*)
    1.21   val thy = @{theory Test};
    1.22   val rls = Test_simplify;
    1.23 - val t = (Thm.term_of o the o (TermC.parse thy)) "(-4) / 2";
    1.24 + val t = TermC.parseNEW'' thy "(-4) / 2";
    1.25  
    1.26  val SOME (_, t) = eval_cancel "xxx" \<^const_name>\<open>divide\<close> t thy;
    1.27  
    1.28  (*--------------(5): reproduce (1) with simpler term: ------------*)
    1.29 - val t = (Thm.term_of o the o (TermC.parse thy)) "(3+5)/2";
    1.30 + val t = TermC.parseNEW'' thy "(3+5)/2::real";
    1.31  case rewrite_set_ thy false rls t of
    1.32    SOME (t', []) =>
    1.33      if UnparseC.term t' = "4" then ()
    1.34      else error "rewrite_set_ (3+5)/2 changed 1"
    1.35  | _ => error "rewrite_set_ (3+5)/2 changed 2";
    1.36  
    1.37 - val t = (Thm.term_of o the o (TermC.parse thy)) "(3+1+2*x)/2";
    1.38 + val t = TermC.parseNEW'' thy "(3+1+2*x)/2::real";
    1.39  case rewrite_set_ thy false rls t of
    1.40    SOME (t', _) =>   (*WAS "x + 2" WITH OLD numerals TOODOO?*)
    1.41      if UnparseC.term t' = "2 + x" then () else error "rewrite_set_ (3+1+2*x)/2 changed 1"
    1.42 @@ -202,7 +202,7 @@
    1.43  
    1.44  (*===================*)
    1.45   Rewrite.trace_on:=false; (*WN130722: =true stopped Test_Isac.thy*)
    1.46 - val t = (Thm.term_of o the o (TermC.parse thy))  "x + (- 1 + -3) / 2";
    1.47 + val t = TermC.parseNEW'' thy  "x + (- 1 + -3) / 2::real";
    1.48  val SOME (res, []) = rewrite_set_ thy false rls t;
    1.49                   (*WAS "x + - 2" WITH OLD numerals TOODOO?*)
    1.50  if UnparseC.term res = "- 2 + x" then () else error "rewrite_set_  x + (- 1 + -3) / 2  changed";
    1.51 @@ -227,17 +227,17 @@
    1.52  " ================= evaluate.sml: calculate_ 2002 =================== ";
    1.53  
    1.54  val thy = @{theory Test};
    1.55 -val t = (Thm.term_of o the o (TermC.parse thy)) "12 / 3";
    1.56 +val t = TermC.parseNEW'' thy "12 / 3";
    1.57  val SOME (thmID,thm) = adhoc_thm thy(the(LibraryC.assoc(KEStore_Elems.get_calcs @{theory},"DIVIDE")))t;
    1.58  val SOME (t,_) = rewrite_ thy tless_true tval_rls true thm t;
    1.59  "12 / 3 = 4";
    1.60  val thy = @{theory Test};
    1.61 -val t = (Thm.term_of o the o (TermC.parse thy)) "4 \<up> 2";
    1.62 +val t = TermC.parseNEW'' thy "4 \<up> 2";
    1.63  val SOME (thmID,thm) = adhoc_thm thy(the(LibraryC.assoc(KEStore_Elems.get_calcs @{theory},"POWER"))) t;
    1.64  val SOME (t,_) = rewrite_ thy tless_true tval_rls true thm t;
    1.65  "4 ^ 2 = 16";
    1.66  
    1.67 - val t = (Thm.term_of o the o (TermC.parse thy)) "((1 + 2) * 4 / 3) \<up> 2";
    1.68 + val t = TermC.parseNEW'' thy "((1 + 2) * 4 / 3) \<up> 2";
    1.69   val SOME (thmID,thm) = adhoc_thm thy (the(LibraryC.assoc(KEStore_Elems.get_calcs @{theory},"PLUS"))) t;
    1.70  "1 + 2 = 3";
    1.71   val SOME (t,_) = rewrite_ thy tless_true tval_rls true thm t;
    1.72 @@ -262,7 +262,7 @@
    1.73   else ();
    1.74  
    1.75  (*13.9.02 *** calc: operator = pow not defined*)
    1.76 -  val t = (Thm.term_of o the o (TermC.parse thy)) "3 \<up> 2";
    1.77 +  val t = TermC.parseNEW'' thy "3 \<up> 2";
    1.78    val SOME (thmID,thm) = 
    1.79        adhoc_thm thy (the(LibraryC.assoc(KEStore_Elems.get_calcs @{theory},"POWER"))) t;
    1.80  (*** calc: operator = pow not defined*)