[isabelle-dev] NEWS: ML antiquotations for type constructors and term constants

[Makarius]

On 22/09/2021 17:50, Makarius wrote:
> On 22/09/2021 14:15, Peter Lammich wrote:
>>
>> Btw, the upper end of complexity for term creation @{mk_term} is
>> something like:
>>
>> @{mk_term "Refine_Basic.bind$(RETURN$(COPY$?p))$?t'"}
>>
>> which looks like a lot of effort to write down in plain ML, or with
>> basic Const antiquotations. In particular, note that all types in the
>> term need to be inferred from the types of ?p and ?t'.
> 
> Here is the direct correspondence to the new antiquotations:

Update for Isabelle/e585e5a906ba:

theory Scratch
  imports Refine_Imperative_HOL.Sepref_Rules Refine_Imperative_HOL.Sepref_Monadify
begin

ML ‹
  fn p => fn t' =>
    @{mk_term "Refine_Basic.bind$(RETURN$(COPY$?p))$?t'"}›

ML ‹
  fn A => fn B => fn p => fn t' =>
    \<^Const>‹Refine_Basic.bind A B for
      \<^Const>‹RETURN A for \<^Const>‹COPY A for p›› t'›
›

end


Thus it is a bit more concise and to the point: no extra nesting of cartouches.

Are there any remaining uses of your alternative antiquotations that are not
covered properly by the new official scheme?


	Makarius