1.1 --- a/src/Tools/isac/Knowledge/Rational.thy	Fri Aug 06 18:27:05 2021 +0200
     1.2 +++ b/src/Tools/isac/Knowledge/Rational.thy	Sun Aug 08 15:21:33 2021 +0200
     1.3 @@ -37,7 +37,7 @@
     1.4                 ((is_ratpolyexp t1) andalso (is_ratpolyexp t2))
     1.5    | is_ratpolyexp (Const (\<^const_name>\<open>divide\<close>,_) $ t1 $ t2) = 
     1.6                 ((is_ratpolyexp t1) andalso (is_ratpolyexp t2))
     1.7 -  | is_ratpolyexp _ = false;
     1.8 +  | is_ratpolyexp t = if TermC.is_num t then true else false;
     1.9  
    1.10  (*("is_ratpolyexp", ("Rational.is_ratpolyexp", eval_is_ratpolyexp ""))*)
    1.11  fun eval_is_ratpolyexp (thmid:string) _