544 |
544 |
545 fun assoc' ([], key) = raise error ("ME_Isa: '"^key^"' not known") |
545 fun assoc' ([], key) = raise error ("ME_Isa: '"^key^"' not known") |
546 | assoc' ((keyi, xi) :: pairs, key) = |
546 | assoc' ((keyi, xi) :: pairs, key) = |
547 if key = keyi then SOME xi else assoc' (pairs, key); |
547 if key = keyi then SOME xi else assoc' (pairs, key); |
548 |
548 |
549 fun assoc_thy (thy:theory') = ((the o assoc')(!theory',thy)) |
549 (*100818 fun assoc_thy (thy:theory') = ((the o assoc')(!theory',thy)) |
550 handle _ => raise error ("ME_Isa: thy '"^thy^"' not in system"); |
550 handle _ => raise error ("ME_Isa: thy '"^thy^"' not in system");*) |
|
551 fun assoc_thy (thy:theory') = theory |
|
552 ((implode o (curry takelast 4) o explode) thy); |
|
553 |
551 (*.associate an rls-identifier with an rls; related to 'fun assoc_rls'; |
554 (*.associate an rls-identifier with an rls; related to 'fun assoc_rls'; |
552 these are NOT compatible to "fun assoc_thm'" in that they do NOT handle |
555 these are NOT compatible to "fun assoc_thm'" in that they do NOT handle |
553 overlays by re-using an identifier in different thys.*) |
556 overlays by re-using an identifier in different thys.*) |
554 fun assoc_rls (rls:rls') = ((#2 o the o assoc')(!ruleset',rls)) |
557 fun assoc_rls (rls:rls') = ((#2 o the o assoc')(!ruleset',rls)) |
555 handle _ => raise error ("ME_Isa: '"^rls^"' not in system"); |
558 handle _ => raise error ("ME_Isa: '"^rls^"' not in system"); |