1.1 --- a/test/Tools/isac/ProgLang/evaluate.sml	Tue May 24 16:47:31 2022 +0200
     1.2 +++ b/test/Tools/isac/ProgLang/evaluate.sml	Thu May 26 12:44:51 2022 +0200
     1.3 @@ -131,13 +131,14 @@
     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 ctxt = (ThyC.id_to_ctxt "Test")
     1.9 + val t = TermC.parseNEW' ctxt "6 / 2";
    1.10   val rls = Test_simplify;
    1.11   val (t,_) = the (rewrite_set_ thy false rls t);
    1.12  (*val t = Free ("3", "Real.real") : term*)
    1.13  
    1.14  (*--------------(3): is_num works ?: -------------------------------------*)
    1.15 - val t = (Thm.term_of o the o (TermC.parse @{theory Test})) "2 is_num";
    1.16 + val t = TermC.parseNEW' ctxt "2 is_num";
    1.17   TermC.atomty t;
    1.18   rewrite_set_ @{theory Test} false tval_rls t;
    1.19  (*val it = SOME (Const (\<^const_name>\<open>True\<close>, "bool"),[]) ... works*)
    1.20 @@ -153,19 +154,19 @@
    1.21   Rewrite.trace_on := false; (*true false*)
    1.22   val thy = @{theory Test};
    1.23   val rls = Test_simplify;
    1.24 - val t = (Thm.term_of o the o (TermC.parse thy)) "(-4) / 2";
    1.25 + val t = TermC.parseNEW' ctxt "(-4) / 2";
    1.26  
    1.27  val SOME (_, t) = eval_cancel "xxx" \<^const_name>\<open>divide\<close> t thy;
    1.28  
    1.29  (*--------------(5): reproduce (1) with simpler term: ------------*)
    1.30 - val t = (Thm.term_of o the o (TermC.parse thy)) "(3+5)/2";
    1.31 + val t = TermC.parseNEW' ctxt "(3+5)/(2::real)";
    1.32  case rewrite_set_ thy false rls t of
    1.33    SOME (t', []) =>
    1.34      if UnparseC.term t' = "4" then ()
    1.35      else error "rewrite_set_ (3+5)/2 changed 1"
    1.36  | _ => error "rewrite_set_ (3+5)/2 changed 2";
    1.37  
    1.38 - val t = (Thm.term_of o the o (TermC.parse thy)) "(3+1+2*x)/2";
    1.39 + val t = TermC.parseNEW' ctxt "(3+1+2*x)/(2::real)";
    1.40  case rewrite_set_ thy false rls t of
    1.41    SOME (t', _) =>
    1.42      if UnparseC.term t' = "2 + x" then () else error "rewrite_set_ (3+1+2*x)/2 changed 1"
    1.43 @@ -203,7 +204,7 @@
    1.44  
    1.45  (*===================*)
    1.46   Rewrite.trace_on:=false; (*WN130722: =true stopped Test_Isac.thy*)
    1.47 - val t = (Thm.term_of o the o (TermC.parse thy))  "x + (- 1 + -3) / 2";
    1.48 + val t = TermC.parseNEW' ctxt "x + (- 1 + -3) / (2::real)";
    1.49  val SOME (res, []) = rewrite_set_ thy false rls t;
    1.50  if UnparseC.term res = "- 2 + x" then () else error "rewrite_set_  x + (- 1 + -3) / 2  changed";
    1.51  "x + (-4) / 2";						
    1.52 @@ -227,17 +228,17 @@
    1.53  " ================= evaluate.sml: calculate_ 2002 =================== ";
    1.54  
    1.55  val thy = @{theory Test};
    1.56 -val t = (Thm.term_of o the o (TermC.parse thy)) "12 / 3";
    1.57 + val t = TermC.parseNEW' ctxt "12 / 3";
    1.58  val SOME (thmID,thm) = adhoc_thm thy(the(LibraryC.assoc(KEStore_Elems.get_calcs @{theory},"DIVIDE")))t;
    1.59  val SOME (t,_) = rewrite_ thy tless_true tval_rls true thm t;
    1.60  "12 / 3 = 4";
    1.61  val thy = @{theory Test};
    1.62 -val t = (Thm.term_of o the o (TermC.parse thy)) "4 \<up> 2";
    1.63 + val t = TermC.parseNEW' ctxt "4 \<up> 2";
    1.64  val SOME (thmID,thm) = adhoc_thm thy(the(LibraryC.assoc(KEStore_Elems.get_calcs @{theory},"POWER"))) t;
    1.65  val SOME (t,_) = rewrite_ thy tless_true tval_rls true thm t;
    1.66  "4 ^ 2 = 16";
    1.67  
    1.68 - val t = (Thm.term_of o the o (TermC.parse thy)) "((1 + 2) * 4 / 3) \<up> 2";
    1.69 + val t = TermC.parseNEW' ctxt "((1 + 2) * 4 / 3) \<up> 2";
    1.70   val SOME (thmID,thm) = adhoc_thm thy (the(LibraryC.assoc(KEStore_Elems.get_calcs @{theory},"PLUS"))) t;
    1.71  "1 + 2 = 3";
    1.72   val SOME (t,_) = rewrite_ thy tless_true tval_rls true thm t;
    1.73 @@ -262,7 +263,7 @@
    1.74   else ();
    1.75  
    1.76  (*13.9.02 *** calc: operator = pow not defined*)
    1.77 -  val t = (Thm.term_of o the o (TermC.parse thy)) "3 \<up> 2";
    1.78 +  val t = TermC.parseNEW' ctxt  "3 \<up> 2";
    1.79    val SOME (thmID,thm) = 
    1.80        adhoc_thm thy (the(LibraryC.assoc(KEStore_Elems.get_calcs @{theory},"POWER"))) t;
    1.81  (*** calc: operator = pow not defined*)