tuned;

--- a/src/Pure/more_pattern.ML	Fri Nov 21 18:14:39 2014 +0100
+++ b/src/Pure/more_pattern.ML	Fri Nov 21 22:59:32 2014 +0100
@@ -44,7 +44,8 @@
   in msub 0 obj end;
 
 fun first_order (Abs (_, _, t)) = first_order t
-  | first_order (t $ u) = first_order t andalso first_order u andalso not (is_Var t)
+  | first_order (Var _ $ _) = false
+  | first_order (t $ u) = first_order t andalso first_order u
   | first_order _ = true;
 
 fun pattern (Abs (_, _, t)) = pattern t