[isabelle] Syntax.string_of_term changed in Isabelle2013



In Isabelle2012 the function

   fun term_to_str t = Print_Mode.setmp [] (Syntax.string_of_term
     (Proof_Context.init_global (Thy_Info.get_theory "Isac"))) t;

   term_to_string @{term "a+1::int"}

delivered

   "a+1": string

which we need for checks in our test suite.

In Isabelle2013 the respective functions in "Syntax" deliver strings apparently for the fontend ( "<markup> ..."). Where do we get a (combination of) function(s) with signature

   : _ -> term -> string

in Isabelle2013 ?


PS: We cound't find an answer neither in isar-ref.pdf "7.1.Printing logical entities" nor in implementation.pdf "3.2.Parsing and unparsing" (the FIXME might concern our question --- nevertheless, thanks for the ever-increasing quality of the manuals !!!).





This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.