| changeset 59027 | f9bee88c5912 |
| parent 59026 | 30b8a5825a9c |
| child 59095 | 3100a7b1c092 |
--- 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