1.1 --- a/src/Tools/isac/calcelems.sml	Sat Feb 24 11:14:56 2018 +0100
     1.2 +++ b/src/Tools/isac/calcelems.sml	Sat Feb 24 16:09:24 2018 +0100
     1.3 @@ -259,6 +259,8 @@
     1.4  fun thy2ctxt thy = Proof_Context.init_global thy;(*FIXXXME thy-ctxt*)
     1.5  
     1.6  fun term2str t = term_to_string' (thy2ctxt' "Isac") t;
     1.7 +fun t2str thy t = term_to_string' (thy2ctxt thy) t;
     1.8 +fun ts2str thy ts = ts |> map (t2str thy) |> strs2str';
     1.9  fun terms2strs ts = map term2str ts;
    1.10  (*terms2strs [t1,t2] = ["1 + 2", "abc"];*)
    1.11  val terms2str = strs2str o terms2strs;
    1.12 @@ -266,6 +268,7 @@
    1.13  val terms2str' = strs2str' o terms2strs;
    1.14  (*terms2str' [t1,t2] = "[1 + 2,abc]";*)
    1.15  
    1.16 +
    1.17  fun termopt2str (SOME t) = "(SOME " ^ term2str t ^ ")"
    1.18    | termopt2str NONE = "NONE";
    1.19