# [isabelle] Query about instantiating theorems in Isabelle/ML

Dear Isabelle/ML experts,
Suppose I have a lemma:
lemma foo: "(x::int) = y+z ==> x - y = z" sorry

`I want to instantiate y to 1. In Isabelle/Isar I can do this easily by
``foo[of _ 1] or foo[where y=1]. How can I do such things in Isabelle/ML?
`

`I believe the answer should have something to do with the
``Drule.instantiate' method in drule.ML, but I don't know how to use this
``method properly in my case.
`

`If variables in foo don't have type restrictions, then the following
``would work:
`
lemma foo1: "x = y+z ==> x - y = z" sorry
ML{*

`Drule.instantiate' [SOME @{ctyp "int"}] [NONE,SOME @{cterm "(1::int)"}]
``@{thm foo1};
`*}
However, with foo,
ML{*

`Drule.instantiate' [SOME @{ctyp "int"}] [NONE,SOME @{cterm "(1::int)"}]
``@{thm foo};
`*}
Isabelle/ML will complain:
exception TYPE raised (line 810 of "drule.ML"):
instantiate': more instantiations than variables in thm
int
1
Many thanks in advance,
Wenda
--
Wenda Li
PhD Candidate
Computer Laboratory
University of Cambridge

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