# [isabelle] odd type error message

```Here I have a simple goal and tactic:

> > Goal   "j <= (i :: nat) --> k < j --> i - j + k < i"
# ;
### Obsolete goal command encountered
Level 0 (1 subgoal)
j <= i --> k < j --> i - j + k < i
1. j <= i --> k < j --> i - j + k < i
val it = [] : Thm.thm list
> by (induct_tac "i" 1);
Level 1 (2 subgoals)
j <= i --> k < j --> i - j + k < i
1. j <= 0 --> k < j --> 0 - j + k < 0
2. !!n. j <= n --> k < j --> n - j + k < n
==> j <= Suc n --> k < j --> Suc n - j + k < Suc n
val it = () : unit

but trying to convert the same proof into Isar I get

```
lemma mpl_lem [rule_format] : "j <= (i :: nat) --> k < j --> i - j + k < i" ;
```proof (prove): step 0

goal (1 subgoal):
1. j <= i --> k < j --> i - j + k < i
variables:
i, j, k :: nat
>   apply (induct_tac "i" 1) ;
proof (prove): step 0

goal (1 subgoal):
1. j <= i --> k < j --> i - j + k < i
variables:
i, j, k :: nat
*** Type unification failed: Clash of types "nat" and "fun"
***
*** Cannot meet type constraint:
***
*** Term:  (i::nat) :: nat
*** Type:  nat => bool
***
*** At command "apply" (line 428 of stdin).

Does anyone have any ideas about what might be happening here?

Thanks for any help

Jeremy

```

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