diff -r dfec2cf32f77 -r 862f35fdb091 src/Tools/isac/calcelems.sml
--- a/src/Tools/isac/calcelems.sml	Thu Aug 19 12:00:46 2010 +0200
+++ b/src/Tools/isac/calcelems.sml	Thu Aug 19 12:08:42 2010 +0200
@@ -136,12 +136,13 @@
 
 (*ctxt for retrieval of all thms in HOL; FIXME make this local?*)
 (*val ctxt_HOL = ProofContext.init_global (theory "Complex_Main");*)
-val ctxt_HOL = thy2ctxt' "Complex_Main";
+(*val ctxt_HOL = thy2ctxt' "Complex_Main";*)
 (*lazy ctxt for retrieval of all thms used in isac; FIXME make this local?*)
-fun ctxt_Isac _  = thy2ctxt' "Isac";
-fun Isac _ = ProofContext.theory_of (ctxt_Isac"");
+(*fun ctxt_Isac _  = thy2ctxt' "Isac";*)
+fun Isac _ = ProofContext.theory_of (thy2ctxt' "Isac");
 
-val e_rule = Thm ("refl", ProofContext.get_thm ctxt_HOL "refl" );
+val e_rule = 
+    Thm ("refl", ProofContext.get_thm (thy2ctxt' "Complex_Main") "refl" );
 fun id_of_thm (Thm (id, _)) = id
   | id_of_thm _ = raise error "id_of_thm";
 fun thm_of_thm (Thm (_, thm)) = thm
@@ -599,13 +600,13 @@
     "SOME " ^ (Sign.string_of_term (sign_of(assoc_thy "Isac.thy")) t)
   | termopt2str NONE = "NONE";*)
 fun termopt2str (SOME t) = 
-    "SOME " ^ (Syntax.string_of_term (ctxt_Isac"") t)
+    "SOME " ^ (Syntax.string_of_term (thy2ctxt' "Isac") t)
   | termopt2str NONE = "NONE";
-fun term2str t = Syntax.string_of_term (ctxt_Isac"") t;
+fun term2str t = Syntax.string_of_term (thy2ctxt' "Isac") t;
 fun terms2str ts= (strs2str o (map (Syntax.string_of_term 
-					(ctxt_Isac"")))) ts;
+					(thy2ctxt' "Isac")))) ts;
 (*fun type2str typ = Sign.string_of_typ (sign_of (assoc_thy "Isac.thy")) typ;*)
-fun type2str typ = Syntax.string_of_typ (ctxt_Isac"") typ;
+fun type2str typ = Syntax.string_of_typ (thy2ctxt' "Isac") typ;
 val string_of_typ = type2str;
 
 fun subst2str (s:subst) =