# [isabelle] Isabelle2015-RC1: Rule instantiation in Eisbach

Dear Eisbach developers,

`First of all, thanks for designing and implementing Eisbach. Unfortunately, I am
``struggling with instantiating variables in rules when I write my own proof methods in Eisbach.
`
Abstractly,
1. I select a rule R by matching a list L of theorems against a term, and

`2. then instantiate a variable in R with a term obtained by matching the conclusion
``against a pattern.
`

`Unfortunately, I always get the error "More instantiations than variables in theorem"
``although all the theorems in the list L contain at least one variable. I do not know where
``this error comes from. Below is a small example:
`
theory Scratch imports Main "~~/src/HOL/Eisbach/Eisbach_Tools" begin
consts foo :: "'a â 'a â 'a â bool"
lemma my_thms: "foo x y z â z â y" "foo x y y â x â z" sorry
lemma "âz. A z â B"
apply(
match concl in "f x y" for f x y â â
match my_thms in R:"PROP P â f u v" for P u v â â
rule R[of x]
â
â
)
oops
end
Thanks for any help,
Andreas

`PS: I am trying to build something similar to the apply_split method in the Eisbach paper
``presented at ITP2014.
`

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