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.
_______________________________________________
Isabelle-dev mailing list
[email protected]
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
