src/Tools/isac/calcelems.sml
branchisac-update-Isa09-2
changeset 38042 26f3832d96b2
parent 38036 02a9b2540eb7
child 38050 4c52ad406c20
equal deleted inserted replaced
38041:850aaf5b3744 38042:26f3832d96b2
   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))