[isabelle] of/where with dummy-patterns



Hi list,

more or less intuitively, I used the of-attribute with dummy-patterns,
e.g.  
  thm imp_refl[of "undefined _ _"]

inside a proof, this works fine. However, outside a proof, I get the
error message 
  Duplicate fixed variable(s): "uu_"

The same behaviour for "where".

Is the of-attribute supposed to work with dummy-patterns or
do they only work by accident within proofs?

If the latter is the case:
  FEATURE REQUEST: Dummy patterns with "of" and "where"!

Best,
  Peter

==============================================
Example:

theory Scratch
imports Main 
begin
  thm imp_refl[of "undefined _ _"]   (* Duplicate fixed variable(s):
"uu_" *)
  context begin
    thm imp_refl[of "undefined _ _"] (* Duplicate fixed variable(s):
"uu_" *)
  end

  notepad begin
    thm imp_refl[of "undefined _ _"] (* undefined ?uu5 ?uua5 â
undefined ?uu5 ?uua5 *)
  end






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