# [isabelle] Why does unfold fail to work?

Here's a snippet from a proof. How can I force Isabelle to unfold the
definition?
from a2 have "deg R (ring.coeff_list_to_poly R l) ≥ (length l) - 1"
(*
goal (1 subgoal):
1. length l - 1 ≤ deg R (ring.coeff_list_to_poly R l)
*)
apply (unfold deg_def bound_def)
(* Unfolds successfully.
goal (1 subgoal):
1. l ! (length l - 1) ≠ \zero
length l - 1 ≤ (LEAST n. ∀m>n. coeff (UP R) (*ring.coeff_list_to_poly*
R l) m = \zero)
*)
apply (unfold *ring.coeff_list_to_poly_def*)
(*Failed to apply proof method*)
For reference:
definition (in ring) *coeff_list_to_poly*::"'a list ⇒ 'a polytype"
where "coeff_list_to_poly l = (λn. if (n < length l) then (l ! n) else
\zero)"

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