<html>
  <head>
    <meta content="text/html; charset=ISO-8859-1"
      http-equiv="Content-Type">
  </head>
  <body bgcolor="#FFFFFF" text="#000000">
    On 10/19/2012 04:35 PM, Makarius wrote:
    <blockquote
cite="mid:alpine.LNX.2.00.1210191634360.14042@macbroy21.informatik.tu-muenchen.de"
      type="cite">On Fri, 19 Oct 2012, Lukas Bulwahn wrote:
      <br>
      <br>
      <blockquote type="cite">
        <blockquote type="cite">Operations like Simplifier.context,
          Simplifier.inherit_context should help here.  Once that is
          repaired, I will see if the warning can now be made an error
          that is more explicit about the reasons.
          <br>
          <br>
        </blockquote>
        I am certainly in favour of this. First, tool developers mainly
        react on errors with test runs, but do not see the warnings.
        Secondly, users do not know who to report those warnings and do
        not know if they are caused by their scripts or the tools.
        <br>
      </blockquote>
      <br>
      Historically, the weak warning was a necessity due to too many
      simprocs still not working with the context.
      <br>
      <br>
      Let's hope that it can be easily switched to an explicit error
      after so many years now.
      <br>
      <br>
    </blockquote>
    On the weekend, I had a look at this issue in the
    set_comprehension_pointfree simproc (cf. changeset 6250121bfffb) and
    already noticed what could make things difficult turning this into
    an error.<br>
    <br>
    Two examples:<br>
    - the hypsubst_tac internally uses the simplifier, but the interface
    does not allow to pass the current simpset to this tactic.<br>
    - An implementer has to avoid certain functions, such as<span
      style="color:#cc0000;"> Raw_Simplifier.rewrite</span>, that assume
    to be used only in a non-nested context.<br>
    <br>
    <br>
    Lukas<br>
  </body>
</html>