# [isabelle] No such variable

Hi,
I have a small feature request: I have a large list of theorems that I'm giving to blast. To simplify blast's search space, I want to fix all of the variables in my theorem list. However, some of the theorems contain only a proper subset of the variables I'm fixing. This causes Isabelle to report a "no such variable" error, even though all of the variables I'm fixing occur in at least one of the theorems.
Below is a simplified example of the error I'm hitting:
theory NoSuchVar
imports Main
begin
lemma L1: "x = x" by auto
lemma L2: "y = y" by auto
lemmas both = L1 L2
thm both[where x=x and y=y] -- {* reports "no such variable" error *}
end
Could this behavior be changed such that the error is reported only when a variable occurs in none of the theorems?
I'm using Isabelle2011-1.
Thanks,
John

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