[isabelle] Lost indexname in instantiated theorem: Eisbach messes up "of" and "where" attributes, when instantiating with "TYPE(...)"



Hi List.

Consider the following theory, where I use the of and where attributes
to instantiate a variable to "TYPE(nat)".
Without Eisbach included, everything is fine. With Eisbach included, I
get the error "Lost indexname in instantiated theorem".

What is going on here, and is there a workaround?

--
  Peter


theory Scratch
imports Main 
  "~~/src/HOL/Eisbach/Eisbach"  (* Remove this line, and everything
works fine *)
begin

  consts f :: "'a â bool"
  lemma foo: "f a â True" by auto

  thm foo[of "TYPE(nat)"]          (* Error: Lost indexname in
instantiated theorem *)
  thm foo[where a = "TYPE(nat)"]   (* Error: Lost indexname in
instantiated theorem *)

end






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