src/Tools/isac/BaseDefinitions/unparseC.sml
changeset 60360 49680d595342
parent 60223 740ebee5948b
child 60500 59a3af532717
     1.1 --- a/src/Tools/isac/BaseDefinitions/unparseC.sml	Tue Aug 10 10:27:15 2021 +0200
     1.2 +++ b/src/Tools/isac/BaseDefinitions/unparseC.sml	Tue Aug 10 11:01:18 2021 +0200
     1.3 @@ -54,7 +54,7 @@
     1.4  \<close>
     1.5  
     1.6  fun term t = term_in_ctxt (ThyC.id_to_ctxt "Isac_Knowledge") t;
     1.7 -fun term_in_thy thy t = term_in_ctxt (ThyC.to_ctxt thy) t;
     1.8 +fun term_in_thy thy t = term_in_ctxt (Proof_Context.init_global thy) t;
     1.9  fun terms_in_thy thy ts = ts |> map (term_in_thy thy) |> strs2str';
    1.10  fun terms_to_strings ts = map term ts;          (* terms_to_strings [t1,t2] = ["1 + 2", "abc"]; *)
    1.11  val terms = strs2str o terms_to_strings;        (* terms  [t1,t2] = "[\"1 + 2\",\"abc\"]";      *)