1.1 --- a/test/Tools/isac/ProgLang/evaluate.sml	Tue Jul 13 15:28:43 2021 +0200
     1.2 +++ b/test/Tools/isac/ProgLang/evaluate.sml	Thu Jul 15 14:10:18 2021 +0200
     1.3 @@ -166,8 +166,8 @@
     1.4  
     1.5   val t = (Thm.term_of o the o (TermC.parse thy)) "(3+1+2*x)/2";
     1.6  case rewrite_set_ thy false rls t of
     1.7 -  SOME (t', _) => 
     1.8 -    if UnparseC.term t' = "x + 2" then () else error "rewrite_set_ (3+1+2*x)/2 changed 1"
     1.9 +  SOME (t', _) =>   (*WAS "x + 2" WITH OLD numerals TOODOO?*)
    1.10 +    if UnparseC.term t' = "2 + x" then () else error "rewrite_set_ (3+1+2*x)/2 changed 1"
    1.11  | _ => error "rewrite_set_ (3+1+2*x)/2 changed 2";
    1.12  
    1.13   Rewrite.trace_on:=false; (*=true3.6.03*)
    1.14 @@ -204,7 +204,8 @@
    1.15   Rewrite.trace_on:=false; (*WN130722: =true stopped Test_Isac.thy*)
    1.16   val t = (Thm.term_of o the o (TermC.parse thy))  "x + (-1 + -3) / 2";
    1.17  val SOME (res, []) = rewrite_set_ thy false rls t;
    1.18 -if UnparseC.term res = "x + - 2" then () else error "rewrite_set_  x + (-1 + -3) / 2  changed";
    1.19 +                 (*WAS "x + - 2" WITH OLD numerals TOODOO?*)
    1.20 +if UnparseC.term res = "- 2 + x" then () else error "rewrite_set_  x + (-1 + -3) / 2  changed";
    1.21  "x + (-4) / 2";						
    1.22  (*
    1.23  ### trying calc. 'cancel'