1.1 --- a/test/Tools/isac/ProgLang/evaluate.sml	Tue Jun 01 15:41:23 2021 +0200
     1.2 +++ b/test/Tools/isac/ProgLang/evaluate.sml	Sat Jul 03 16:21:07 2021 +0200
     1.3 @@ -167,8 +167,7 @@
     1.4   val t = (Thm.term_of o the o (TermC.parse thy)) "(3+1+2*x)/2";
     1.5  case rewrite_set_ thy false rls t of
     1.6    SOME (t', _) => 
     1.7 -    if UnparseC.term t' = "x + (1 / 2 + 3 / 2)" (*ERROR should be : 2 * x  SEE ABOVE*) then ()
     1.8 -    else error "rewrite_set_ (3+1+2*x)/2 changed 1"
     1.9 +    if UnparseC.term t' = "x + 2" then () else error "rewrite_set_ (3+1+2*x)/2 changed 1"
    1.10  | _ => error "rewrite_set_ (3+1+2*x)/2 changed 2";
    1.11  
    1.12   Rewrite.trace_on:=false; (*=true3.6.03*)