[isabelle-dev] produce term patterns

[Makarius]

On Fri, 3 Sep 2010, Walther Neuper wrote:

> that one should query The Isabelle Programming Tutorial before asking in 
> isabelle-dev@; sorry for having failed to do this this time.

The tutorial is helpful in many situations, but many things are not fully 
canonical, i.e. you need to cross-check with other sources of information.


> That is exactly what we need, ...
>
> ML {* print_depth 99;
> val ctxt = ProofContext.init_global  @{theory};
> ProofContext.read_term_pattern ctxt "matches (?a + ?b * bdv^2 = (0::real)) 
> equ";
> *}

BTW, the "global" in ProofContext.init_global indicates that this is a 
somewhat unusual operation to be used only as last resort, when no proper 
local context is available.  Here you have one, which is the context of 
the 'ML' command.

So you really should use proper @{context} here, not the raw background 
@{theory}.  Of course, these antiquotations only work for individual tests 
-- the context is that of the compile-time of the ML command.  In 
production code you need to abstract over the "ctxt", passing through the 
value that you get from the surrounding system infrastructure (i.e. 
concrete syntax wrappers of proof methods etc.).


 	Makarius