src/Tools/isac/calcelems.sml
branchisac-update-Isa09-2
changeset 37927 183e35109dda
parent 37924 6c53fe2519e5
child 37928 dfec2cf32f77
     1.1 --- a/src/Tools/isac/calcelems.sml	Wed Aug 18 13:55:23 2010 +0200
     1.2 +++ b/src/Tools/isac/calcelems.sml	Wed Aug 18 16:03:27 2010 +0200
     1.3 @@ -546,8 +546,11 @@
     1.4    | assoc' ((keyi, xi) :: pairs, key) =
     1.5        if key = keyi then SOME xi else assoc' (pairs, key);
     1.6  
     1.7 -fun assoc_thy (thy:theory') = ((the o assoc')(!theory',thy))
     1.8 -  handle _ => raise error ("ME_Isa: thy '"^thy^"' not in system");
     1.9 +(*100818 fun assoc_thy (thy:theory') = ((the o assoc')(!theory',thy))
    1.10 +  handle _ => raise error ("ME_Isa: thy '"^thy^"' not in system");*)
    1.11 +fun assoc_thy (thy:theory') = theory 
    1.12 +  ((implode o (curry takelast 4) o explode) thy);
    1.13 +
    1.14  (*.associate an rls-identifier with an rls; related to 'fun assoc_rls';
    1.15     these are NOT compatible to "fun assoc_thm'" in that they do NOT handle
    1.16     overlays by re-using an identifier in different thys.*)