1.1 --- a/src/Tools/isac/Knowledge/Rational.thy	Thu Apr 29 12:43:50 2021 +0200
     1.2 +++ b/src/Tools/isac/Knowledge/Rational.thy	Thu Apr 29 14:13:11 2021 +0200
     1.3 @@ -213,9 +213,10 @@
     1.4  subsubsection \<open>Factor out gcd for cancellation\<close>
     1.5  ML \<open>
     1.6  fun check_fraction t =
     1.7 -  let val Const ("Rings.divide_class.divide", _) $ numerator $ denominator = t
     1.8 -  in SOME (numerator, denominator) end
     1.9 -  handle Bind => NONE
    1.10 +  case t of
    1.11 +    Const ("Rings.divide_class.divide", _) $ numerator $ denominator
    1.12 +      => SOME (numerator, denominator)
    1.13 +  | _ => NONE
    1.14  
    1.15  (* prepare a term for cancellation by factoring out the gcd
    1.16    assumes: is a fraction with outmost "/"*)