Why do I get this exception on an induction rule for a lemma?

I am trying to prove the following lemma (which is the meaning formula for the addition of two Binary numerals). It goes like this :

lemma (in th2) addMeaningF_2: "∀m. m ≤ n ⟹ (m = (len x + len y) ⟹ (evalBinNum_1 (addBinNum x y) = plus (evalBinNum_1 x) (evalBinNum_1 y)))"

I am trying to perform strong induction. When I apply(induction n rule: less_induct) on the lemma, it throws an error.

exception THM 0 raised (line 755 of "drule.ML"):
  infer_instantiate_types: type ?'a of variable ?a
  cannot be unified with type 'b of term n
  (⋀x. (⋀y. y < x ⟹ ?P y) ⟹ ?P x) ⟹ ?P ?a

Can anyone explain this?

Edit: For more context

locale th2 = th1 +
  fixes 
    plus :: "'a ⇒ 'a ⇒ 'a"
  assumes
     arith_1: "plus n zero = n"
    and plus_suc: "plus n (suc m) = suc ( plus n m)"

len and evalBinNum_1 are both recursive functions len gives us the length of a given binary numeral, while evalBinNum_1 evaluates binary numerals.

fun (in th2) evalBinNum_1 :: "BinNum ⇒ 'a"
  where 
    "evalBinNum_1 Zero = zero"|
    "evalBinNum_1 One = suc(zero)"|
    "evalBinNum_1 (JoinZero x) = plus (evalBinNum_1 x) (evalBinNum_1 x)"|
    "evalBinNum_1 (JoinOne x) = plus (plus (evalBinNum_1 x) (evalBinNum_1 x)) (suc zero)"

Solution

The problem is that Isabelle cannot infer the type of n (or the bound occurrence of m) when trying to use the induction rule less_induct. You might want to add a type annotation such as (n::nat) in your lemma. For the sake of generality, you might want to state that the type of n is an instance of the class wellorder, that is, (n::'a::wellorder). On another subject, I think there is a logical issue with your lemma statement: I guess you actually mean ∀m. m ≤ (n::nat) ⟶ ... ⟶ ... or, equivalently, ⋀m. m ≤ (n::nat) ⟹ ... ⟹ .... Finally, it would be good to know the context of your problem (e.g., there seems to be a locale th2 involved) for a more precise answer.