[isabelle] Isabelle Cookbook example

Hi all,

I'm reading the Isabelle Cookbook and trying some of the examples provided.
There's something I don't quite understand: I'm looking at the June 8, 2010
version and on page 22, there's an example on implementing a custom

val parser = Args.context

fun term_pat (ctxt, str) =


Then there's an example on calling this antiquotation:

@{term_pat "Suc (?x::nat)"}

Since term_pat takes two arguments ctxt and str, how come the antiquotation
@{term_pat "Suc (?x::nat)"} only has one argument?

Thanks for the help.


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