equal
deleted
inserted
replaced
45 -> bool)) (* if t1 <= t2 then true else false *) |
45 -> bool)) (* if t1 <= t2 then true else false *) |
46 list); (* association list *) |
46 list); (* association list *) |
47 fun assoc' ([], key) = raise ERROR ("ME_Isa: \"" ^ key ^ "\" not known") |
47 fun assoc' ([], key) = raise ERROR ("ME_Isa: \"" ^ key ^ "\" not known") |
48 | assoc' ((keyi, xi) :: pairs, key) = |
48 | assoc' ((keyi, xi) :: pairs, key) = |
49 if key = keyi then SOME xi else assoc' (pairs, key); |
49 if key = keyi then SOME xi else assoc' (pairs, key); |
50 fun assoc_rew_ord ro = ((the o assoc') (! rew_ord',ro)) |
50 fun assoc_rew_ord ro = ((the o assoc') (! rew_ord', ro)) |
51 handle _ => raise ERROR ("ME_Isa: rew_ord '" ^ ro ^ "' not in system"); |
51 handle ERROR _ => raise ERROR ("ME_Isa: rew_ord '" ^ ro ^ "' not in system"); |
52 |
52 |
53 end |
53 end |