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