equal
deleted
inserted
replaced
344 |
344 |
345 |
345 |
346 (*rewrite orders, also stored in 'type met' and type 'and rls' |
346 (*rewrite orders, also stored in 'type met' and type 'and rls' |
347 The association list is required for 'rewrite.."rew_ord"..' |
347 The association list is required for 'rewrite.."rew_ord"..' |
348 WN0509 tests not well-organized: see smltest/Knowledge/termorder.sml*) |
348 WN0509 tests not well-organized: see smltest/Knowledge/termorder.sml*) |
349 val rew_ord' = |
349 val rew_ord' = |
350 ref ([]:(rew_ord' * (*the key for the association list *) |
350 Unsynchronized.ref |
|
351 ([]:(rew_ord' * (*the key for the association list *) |
351 (subst (*the bound variables - they get high order*) |
352 (subst (*the bound variables - they get high order*) |
352 -> (term * term) (*(t1, t2) to be compared *) |
353 -> (term * term) (*(t1, t2) to be compared *) |
353 -> bool)) (*if t1 <= t2 then true else false *) |
354 -> bool)) (*if t1 <= t2 then true else false *) |
354 list); (*association list *) |
355 list); (*association list *) |
355 rew_ord' := overwritel (!rew_ord', [("e_rew_ord", e_rew_ord), |
356 rew_ord' := overwritel (!rew_ord', [("e_rew_ord", e_rew_ord), |