[isabelle-dev] produce term patterns

[Walther Neuper]

Makarius,

thanks for the warning ...

On 09/03/2010 01:31 PM, Makarius wrote:
> On Fri, 3 Sep 2010, Walther Neuper wrote:
> [...]
>> 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.
>
... but we are still struggling to bring the old code alive in the 
Isabelle2009 world. If the code runs again, then we shall take advantage 
of all the wonderful services of present Isabelle and then with pleasure 
follow your recommendations ...
> 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 
Walther

PS: I have already some general questions waiting for the happy event 
when the code is alive again.