1.1 --- a/src/Tools/isac/Isac_Mathengine.thy	Wed Aug 18 13:55:23 2010 +0200
     1.2 +++ b/src/Tools/isac/Isac_Mathengine.thy	Wed Aug 18 16:03:27 2010 +0200
     1.3 @@ -22,7 +22,6 @@
     1.4  begin
     1.5  
     1.6  ML {* Toplevel.debug := true; *}
     1.7 -
     1.8  use "library.sml"
     1.9  use "calcelems.sml"
    1.10  ML {* check_guhs_unique := true *}
    1.11 @@ -35,6 +34,7 @@
    1.12  
    1.13  use "ME/mstools.sml"
    1.14  use "ME/ctree.sml"
    1.15 +use "ME/ptyps.sml"
    1.16  
    1.17  
    1.18  ML {*
    1.19 @@ -44,7 +44,6 @@
    1.20  
    1.21  
    1.22  (*
    1.23 -use "ME/ptyps.sml"
    1.24  use "ME/generate.sml"
    1.25  use "ME/calchead.sml"
    1.26  use "ME/appl.sml"

     2.1 --- a/src/Tools/isac/calcelems.sml	Wed Aug 18 13:55:23 2010 +0200
     2.2 +++ b/src/Tools/isac/calcelems.sml	Wed Aug 18 16:03:27 2010 +0200
     2.3 @@ -546,8 +546,11 @@
     2.4    | assoc' ((keyi, xi) :: pairs, key) =
     2.5        if key = keyi then SOME xi else assoc' (pairs, key);
     2.6  
     2.7 -fun assoc_thy (thy:theory') = ((the o assoc')(!theory',thy))
     2.8 -  handle _ => raise error ("ME_Isa: thy '"^thy^"' not in system");
     2.9 +(*100818 fun assoc_thy (thy:theory') = ((the o assoc')(!theory',thy))
    2.10 +  handle _ => raise error ("ME_Isa: thy '"^thy^"' not in system");*)
    2.11 +fun assoc_thy (thy:theory') = theory 
    2.12 +  ((implode o (curry takelast 4) o explode) thy);
    2.13 +
    2.14  (*.associate an rls-identifier with an rls; related to 'fun assoc_rls';
    2.15     these are NOT compatible to "fun assoc_thm'" in that they do NOT handle
    2.16     overlays by re-using an identifier in different thys.*)