equal
deleted
inserted
replaced
281 fun canonize_term (Const (s, T) $ t $ u) comms = |
281 fun canonize_term (Const (s, T) $ t $ u) comms = |
282 let |
282 let |
283 val t' = canonize_term t comms; |
283 val t' = canonize_term t comms; |
284 val u' = canonize_term u comms; |
284 val u' = canonize_term u comms; |
285 in |
285 in |
286 if member (op =) comms s andalso Term_Ord.termless (u', t') |
286 if member (op =) comms s andalso is_less (Term_Ord.term_ord (u', t')) |
287 then Const (s, T) $ u' $ t' |
287 then Const (s, T) $ u' $ t' |
288 else Const (s, T) $ t' $ u' |
288 else Const (s, T) $ t' $ u' |
289 end |
289 end |
290 | canonize_term (t $ u) comms = canonize_term t comms $ canonize_term u comms |
290 | canonize_term (t $ u) comms = canonize_term t comms $ canonize_term u comms |
291 | canonize_term (Abs (s, T, t)) comms = Abs (s, T, canonize_term t comms) |
291 | canonize_term (Abs (s, T, t)) comms = Abs (s, T, canonize_term t comms) |