equal
deleted
inserted
replaced
93 fun isLargerTerm ({ordering,orderTerms,...} : parameters) l_r = |
93 fun isLargerTerm ({ordering,orderTerms,...} : parameters) l_r = |
94 not orderTerms orelse not (strictlyLess ordering l_r); |
94 not orderTerms orelse not (strictlyLess ordering l_r); |
95 |
95 |
96 local |
96 local |
97 fun atomToTerms atm = |
97 fun atomToTerms atm = |
98 Term.Fn atm :: |
98 case total Atom.destEq atm of |
99 (case total Atom.sym atm of NONE => [] | SOME atm => [Term.Fn atm]); |
99 NONE => [Term.Fn atm] |
|
100 | SOME (l,r) => [l,r]; |
100 |
101 |
101 fun notStrictlyLess ordering (xs,ys) = |
102 fun notStrictlyLess ordering (xs,ys) = |
102 let |
103 let |
103 fun less x = List.exists (fn y => strictlyLess ordering (x,y)) ys |
104 fun less x = List.exists (fn y => strictlyLess ordering (x,y)) ys |
104 in |
105 in |