1.1 --- a/src/Tools/isac/calcelems.sml	Thu Aug 19 12:00:46 2010 +0200
     1.2 +++ b/src/Tools/isac/calcelems.sml	Thu Aug 19 12:08:42 2010 +0200
     1.3 @@ -136,12 +136,13 @@
     1.4  
     1.5  (*ctxt for retrieval of all thms in HOL; FIXME make this local?*)
     1.6  (*val ctxt_HOL = ProofContext.init_global (theory "Complex_Main");*)
     1.7 -val ctxt_HOL = thy2ctxt' "Complex_Main";
     1.8 +(*val ctxt_HOL = thy2ctxt' "Complex_Main";*)
     1.9  (*lazy ctxt for retrieval of all thms used in isac; FIXME make this local?*)
    1.10 -fun ctxt_Isac _  = thy2ctxt' "Isac";
    1.11 -fun Isac _ = ProofContext.theory_of (ctxt_Isac"");
    1.12 +(*fun ctxt_Isac _  = thy2ctxt' "Isac";*)
    1.13 +fun Isac _ = ProofContext.theory_of (thy2ctxt' "Isac");
    1.14  
    1.15 -val e_rule = Thm ("refl", ProofContext.get_thm ctxt_HOL "refl" );
    1.16 +val e_rule = 
    1.17 +    Thm ("refl", ProofContext.get_thm (thy2ctxt' "Complex_Main") "refl" );
    1.18  fun id_of_thm (Thm (id, _)) = id
    1.19    | id_of_thm _ = raise error "id_of_thm";
    1.20  fun thm_of_thm (Thm (_, thm)) = thm
    1.21 @@ -599,13 +600,13 @@
    1.22      "SOME " ^ (Sign.string_of_term (sign_of(assoc_thy "Isac.thy")) t)
    1.23    | termopt2str NONE = "NONE";*)
    1.24  fun termopt2str (SOME t) = 
    1.25 -    "SOME " ^ (Syntax.string_of_term (ctxt_Isac"") t)
    1.26 +    "SOME " ^ (Syntax.string_of_term (thy2ctxt' "Isac") t)
    1.27    | termopt2str NONE = "NONE";
    1.28 -fun term2str t = Syntax.string_of_term (ctxt_Isac"") t;
    1.29 +fun term2str t = Syntax.string_of_term (thy2ctxt' "Isac") t;
    1.30  fun terms2str ts= (strs2str o (map (Syntax.string_of_term 
    1.31 -					(ctxt_Isac"")))) ts;
    1.32 +					(thy2ctxt' "Isac")))) ts;
    1.33  (*fun type2str typ = Sign.string_of_typ (sign_of (assoc_thy "Isac.thy")) typ;*)
    1.34 -fun type2str typ = Syntax.string_of_typ (ctxt_Isac"") typ;
    1.35 +fun type2str typ = Syntax.string_of_typ (thy2ctxt' "Isac") typ;
    1.36  val string_of_typ = type2str;
    1.37  
    1.38  fun subst2str (s:subst) =