1.1 --- a/src/Tools/isac/ProgLang/Prog_Expr.thy	Sun Aug 22 14:28:38 2021 +0200
     1.2 +++ b/src/Tools/isac/ProgLang/Prog_Expr.thy	Mon Aug 23 12:33:10 2021 +0200
     1.3 @@ -423,9 +423,9 @@
     1.4        let
     1.5          val (T, _) = HOLogic.dest_number t1;
     1.6          val (i1, i2) = (Eval.int_of_numeral t1, Eval.int_of_numeral t2);
     1.7 -        val res_int as (_, (i1', i2')) = Eval.cancel_int (i1, i2);
     1.8 +        val res_int as (d, (i1', i2')) = Eval.cancel_int (i1, i2);
     1.9        in
    1.10 -        if (i1', i2') = (i1, i2) then NONE
    1.11 +        if abs d = 1 andalso (abs i1, abs i2) = (abs i1', abs i2') then NONE
    1.12          else
    1.13            let
    1.14              val res = TermC.mk_frac T res_int;