1.1 --- a/src/Tools/isac/Knowledge/Poly.thy	Tue Mar 19 17:52:36 2019 +0100
     1.2 +++ b/src/Tools/isac/Knowledge/Poly.thy	Wed Mar 20 12:16:48 2019 +0100
     1.3 @@ -187,15 +187,15 @@
     1.4    if (2) then v is a factor on the very right, ev. with exponent.*)
     1.5  fun factor_right_deg (*case 2*)
     1.6  	    (Const ("Groups.times_class.times", _) $ t1 $ (Const ("Atools.pow",_) $ vv $ Free (d, _))) v =
     1.7 -	   if ((vv = v) andalso (TermC.coeff_in t1 v)) then SOME (TermC.int_of_str d) else NONE
     1.8 +	   if vv = v andalso not (TermC.coeff_in t1 v) then SOME (TermC.int_of_str d) else NONE
     1.9    | factor_right_deg (Const ("Atools.pow",_) $ vv $ Free (d,_)) v =
    1.10  	   if (vv = v) then SOME (TermC.int_of_str d) else NONE
    1.11    | factor_right_deg (Const ("Groups.times_class.times",_) $ t1 $ vv) v = 
    1.12 -	   if ((vv = v) andalso (TermC.coeff_in t1 v)) then SOME 1 else NONE
    1.13 +	   if vv = v andalso not (TermC.coeff_in t1 v) then SOME 1 else NONE
    1.14    | factor_right_deg vv v =
    1.15  	  if (vv = v) then SOME 1 else NONE;    
    1.16  fun mono_deg_in m v =  (*case 1*)
    1.17 -	if TermC.coeff_in m v then (*case 1*) SOME 0 else factor_right_deg m v;
    1.18 +	if not (TermC.coeff_in m v) then (*case 1*) SOME 0 else factor_right_deg m v;
    1.19  
    1.20  fun expand_deg_in t v =
    1.21  	let
    1.22 @@ -515,23 +515,18 @@
    1.23  ML \<open>
    1.24  (* is_polyrat_in becomes true, if no bdv is in the denominator of a fraction*)
    1.25  fun is_polyrat_in t v = 
    1.26 -    let
    1.27 +  let
    1.28     	fun finddivide (_ $ _ $ _ $ _) _ = error("is_polyrat_in:")
    1.29  	    (* at the moment there is no term like this, but ....*)
    1.30 -	  | finddivide (Const ("Rings.divide_class.divide",_) $ _ $ b) v = 
    1.31 -            not(TermC.coeff_in b v)
    1.32 -	  | finddivide (_ $ t1 $ t2) v = 
    1.33 -            (finddivide t1 v) orelse (finddivide t2 v)
    1.34 -	  | finddivide (_ $ t1) v = (finddivide t1 v)
    1.35 +	  | finddivide (Const ("Rings.divide_class.divide",_) $ _ $ b) v = not (TermC.coeff_in b v)
    1.36 +	  | finddivide (_ $ t1 $ t2) v = finddivide t1 v orelse finddivide t2 v
    1.37 +	  | finddivide (_ $ t1) v = finddivide t1 v
    1.38  	  | finddivide _ _ = false;
    1.39 -     in finddivide t v end;
    1.40 +  in finddivide t v end;
    1.41      
    1.42 -fun is_expanded_in t v =
    1.43 -    case expand_deg_in t v of SOME _ => true | NONE => false;
    1.44 -fun is_poly_in t v =
    1.45 -    case poly_deg_in t v of SOME _ => true | NONE => false;
    1.46 -fun has_degree_in t v =
    1.47 -    case expand_deg_in t v of SOME d => d | NONE => ~1;
    1.48 +fun is_expanded_in t v = case expand_deg_in t v of SOME _ => true | NONE => false;
    1.49 +fun is_poly_in t v =     case poly_deg_in t v of SOME _ => true | NONE => false;
    1.50 +fun has_degree_in t v =  case expand_deg_in t v of SOME d => d | NONE => ~1;
    1.51  
    1.52  (*.the expression contains + - * ^ only ?
    1.53     this is weaker than 'is_polynomial' !.*)