1.1 --- a/src/Tools/isac/calcelems.sml	Fri May 13 17:19:38 2011 +0200
     1.2 +++ b/src/Tools/isac/calcelems.sml	Sun May 15 10:25:42 2011 +0200
     1.3 @@ -136,12 +136,7 @@
     1.4  fun thy2ctxt' thy' = ProofContext.init_global (Thy_Info.get_theory thy');(*FIXXXME thy-ctxt*)
     1.5  fun thy2ctxt thy = ProofContext.init_global thy;(*FIXXXME thy-ctxt*)
     1.6  
     1.7 -(*ctxt for retrieval of all thms in HOL; FIXME make this local?*)
     1.8 -(*val ctxt_HOL = ProofContext.init_global (Thy_Info.get_theory "Complex_Main");*)
     1.9 -(*val ctxt_HOL = thy2ctxt' "Complex_Main";*)
    1.10 -(*lazy ctxt for retrieval of all thms used in isac; FIXME make this local?*)
    1.11 -(*fun ctxt_Isac _  = thy2ctxt' "Isac";*)
    1.12 -fun Isac _ = ProofContext.theory_of (thy2ctxt' "Isac");
    1.13 +fun Isac _ = ProofContext.theory_of (thy2ctxt' "Isac"); (*@{theory "Isac"}*)
    1.14  
    1.15  val e_rule = Thm ("refl", @{thm refl});
    1.16  fun id_of_thm (Thm (id, _)) = id