Q:

Isabelle Type Error

I am new to Isabelle and doing an Exercise for University. I need to proof a reverse function in Isabelle.
In Haskell the function would look like this:
rev [] = []
rev (x:xs) = rev xs ++ [x]

I now tryed to define this function "rev" in Isabelle. The type list and the function "app" (append)

The Error Isabelle gives me is:
Type unification failed: Clash of types "_
          ⇒ _" and "_ Exercise5.list"

Type error in application: incompatible operand type

Operator:  app (rev xs) ::
  'a Exercise5.list ⇒ 'a Exercise5.list
Operand:   Exercise5.list.Cons ::
  ??'a ⇒ ??'a Exercise5.list ⇒ ??'a Exercise5.list

Where is the Problem? As far as I understand it Isabelle is telling me "Hey buddy app needs 2 arguments of type a' list but this is not the case here" 
but why? xs is clearly of type a' list and with my Cons operator i do make x also a list? 
Thanks for the Help!

A:

Think about where the parenthesis should be put in app rev xs Cons x Nil: Currently you seem to apply the function x on its argument Nil.

