1.1 --- a/src/Tools/isac/calcelems.sml	Tue Aug 17 09:05:51 2010 +0200
     1.2 +++ b/src/Tools/isac/calcelems.sml	Wed Aug 18 13:40:09 2010 +0200
     1.3 @@ -131,12 +131,13 @@
     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  
     1.9  (*ctxt for retrieval of all thms in HOL; FIXME make this local?*)
    1.10 -val ctxt_HOL = ProofContext.init_global (theory "Complex_Main");
    1.11 -val HOL = ProofContext.theory_of ctxt_HOL;
    1.12 +(*val ctxt_HOL = ProofContext.init_global (theory "Complex_Main");*)
    1.13 +val ctxt_HOL = thy2ctxt "Complex_Main";
    1.14  (*lazy ctxt for retrieval of all thms used in isac; FIXME make this local?*)
    1.15 -fun ctxt_Isac _  = ProofContext.init_global (theory "Isac");
    1.16 +fun ctxt_Isac _  = thy2ctxt "Isac";
    1.17  fun Isac _ = ProofContext.theory_of (ctxt_Isac"");
    1.18  
    1.19  val e_rule = Thm ("refl", ProofContext.get_thm ctxt_HOL "refl" );