30 val e_rew_ord = dummy_ord; (* TODO.WN071231 clarify identifiers..e_rew_ordX*) |
30 val e_rew_ord = dummy_ord; (* TODO.WN071231 clarify identifiers..e_rew_ordX*) |
31 val e_rew_ordX = (e_rew_ord', e_rew_ord_) |
31 val e_rew_ordX = (e_rew_ord', e_rew_ord_) |
32 fun to_string (rew_ord', _) = "(" ^ rew_ord' ^ ", _: fn)" |
32 fun to_string (rew_ord', _) = "(" ^ rew_ord' ^ ", _: fn)" |
33 |
33 |
34 type rew_ord' = Rule_Def.rew_ord' |
34 type rew_ord' = Rule_Def.rew_ord' |
35 (* rewrite orders, also stored in 'type met' and type 'and rls' |
|
36 The association list is required for 'rewrite.."rew_ord"..' *) |
|
37 val rew_ord' = Unsynchronized.ref |
|
38 ([("e_rew_ord", e_rew_ord), ("dummy_ord", dummy_ord)] |
|
39 : (rew_ord' * (* the key for the association list *) |
|
40 (subst (* the bound variables - they get high order*) |
|
41 -> (term * term) (* (t1, t2) to be compared *) |
|
42 -> bool)) (* if t1 <= t2 then true else false *) |
|
43 list); (* association list *) |
|
44 |
|
45 fun equal ((id1, _), (id2, _)) = id1 = id2 |
35 fun equal ((id1, _), (id2, _)) = id1 = id2 |
46 |
36 |
47 end |
37 end |