1.1 --- a/src/Tools/isac/calcelems.sml	Wed Aug 18 16:03:27 2010 +0200
     1.2 +++ b/src/Tools/isac/calcelems.sml	Thu Aug 19 12:00:46 2010 +0200
     1.3 @@ -131,13 +131,14 @@
     1.4  (*1.8.02 ad (how to restrict type ???): scr should be usable indepentently
     1.5    from rls, and then contain both Script _AND_ Rfuns !!!*)
     1.6  
     1.7 -fun thy2ctxt thy' = ProofContext.init_global (theory thy'); (*FIXXXME thy-ctxt*)
     1.8 +fun thy2ctxt' thy' = ProofContext.init_global (theory thy');(*FIXXXME thy-ctxt*)
     1.9 +fun thy2ctxt thy = ProofContext.init_global thy;(*FIXXXME thy-ctxt*)
    1.10  
    1.11  (*ctxt for retrieval of all thms in HOL; FIXME make this local?*)
    1.12  (*val ctxt_HOL = ProofContext.init_global (theory "Complex_Main");*)
    1.13 -val ctxt_HOL = thy2ctxt "Complex_Main";
    1.14 +val ctxt_HOL = thy2ctxt' "Complex_Main";
    1.15  (*lazy ctxt for retrieval of all thms used in isac; FIXME make this local?*)
    1.16 -fun ctxt_Isac _  = thy2ctxt "Isac";
    1.17 +fun ctxt_Isac _  = thy2ctxt' "Isac";
    1.18  fun Isac _ = ProofContext.theory_of (ctxt_Isac"");
    1.19  
    1.20  val e_rule = Thm ("refl", ProofContext.get_thm ctxt_HOL "refl" );
    1.21 @@ -548,9 +549,10 @@
    1.22  
    1.23  (*100818 fun assoc_thy (thy:theory') = ((the o assoc')(!theory',thy))
    1.24    handle _ => raise error ("ME_Isa: thy '"^thy^"' not in system");*)
    1.25 -fun assoc_thy (thy:theory') = theory 
    1.26 -  ((implode o (curry takelast 4) o explode) thy);
    1.27 -
    1.28 +fun assoc_thy (thy:theory') = (*FIXME100818 abolish*)
    1.29 +    (theory ((implode o (curry takelast 4) o explode) thy))
    1.30 +    handle _ => raise error ("ME_Isa: thy '" ^ thy ^ "' not in system");
    1.31 +    
    1.32  (*.associate an rls-identifier with an rls; related to 'fun assoc_rls';
    1.33     these are NOT compatible to "fun assoc_thm'" in that they do NOT handle
    1.34     overlays by re-using an identifier in different thys.*)