src/Tools/isac/calcelems.sml
changeset 55443 46613d0a9fc9
parent 55437 9c19751b2ad1
child 55444 ede4248a827b
     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;