1.1 --- a/src/Tools/isac/calcelems.sml Thu Jun 12 21:59:15 2014 +0200
1.2 +++ b/src/Tools/isac/calcelems.sml Fri Jun 13 09:55:49 2014 +0200
1.3 @@ -740,7 +740,7 @@
1.4 val ctxt' = Config.put show_markup false (Proof_Context.init_global thy)
1.5 in Print_Mode.setmp [] (Syntax.string_of_term ctxt') t end;
1.6
1.7 -fun term2str t = term_to_string' (ML_Context.the_generic_context () |> Context.proof_of) t;
1.8 +fun term2str t = term_to_string' (assoc_thy "Isac" |> thy2ctxt) t;
1.9 fun terms2strs ts = map term2str ts;
1.10 (*terms2strs [t1,t2] = ["1 + 2", "abc"];*)
1.11 val terms2str = strs2str o terms2strs;