# HG changeset patch
# User wenzelm
# Date 1416607172 -3600
# Node ID f9bee88c59129c73e715039ea6c99e26c96e3ccb
# Parent  30b8a5825a9c053a57cdb96f749f93e2d4456d6d
tuned;

diff -r 30b8a5825a9c -r f9bee88c5912 src/Pure/more_pattern.ML
--- 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