1.1 --- a/src/Tools/isac/IsacKnowledge/Test.ML	Thu Aug 19 15:41:56 2010 +0200
     1.2 +++ b/src/Tools/isac/IsacKnowledge/Test.ML	Fri Aug 20 12:25:37 2010 +0200
     1.3 @@ -538,13 +538,13 @@
     1.4      if atom t then true else bin_ops_only t;
     1.5  
     1.6  fun polynomial opl t bdVar = (* bdVar TODO *)
     1.7 -    (bin_op t) subset opl andalso (bin_ops_only t);
     1.8 +    subset op = (bin_op t, opl) andalso (bin_ops_only t);
     1.9  
    1.10  fun poly_equ opl bdVar t = is_equation t (* bdVar TODO *) 
    1.11      andalso polynomial opl (equ_lhs t) bdVar 
    1.12      andalso polynomial opl (equ_rhs t) bdVar
    1.13 -    andalso ((varids bdVar) subset (varids (equ_lhs t))
    1.14 -	     orelse(varids bdVar) subset (varids (equ_lhs t)));
    1.15 +    andalso (subset op = (varids bdVar, varids (equ_lhs t)) orelse
    1.16 +             subset op = (varids bdVar, varids (equ_lhs t)));
    1.17  
    1.18  (*fun max is =
    1.19      let fun max_ m [] = m 
    1.20 @@ -563,7 +563,7 @@
    1.21  (*| deg _ _ v (_     (s,"?DUMMY"   ))          =   ..ML-error *) 
    1.22    | deg _ _ v((Const ("Bin.integ_of_bin",_)) $ _ )= 0 
    1.23    | deg addl mul v (h $ t1 $ t2) =
    1.24 -    if(bin_op h)subset addl
    1.25 +    if subset op = (bin_op h, addl)
    1.26      then max (deg addl mul v t1  ,deg addl mul v t2)
    1.27      else (*mul!*)(deg addl mul v t1)+(deg addl mul v t2)
    1.28  in if polynomial (addl @ [mul]) t bdVar