src/Pure/pattern.ML

--- a/src/Pure/pattern.ML	Tue Jul 30 11:12:52 2019 +0200
+++ b/src/Pure/pattern.ML	Tue Jul 30 11:41:39 2019 +0200
@@ -21,6 +21,7 @@
   val match: theory -> term * term -> Type.tyenv * Envir.tenv -> Type.tyenv * Envir.tenv
   val first_order_match: theory -> term * term
     -> Type.tyenv * Envir.tenv -> Type.tyenv * Envir.tenv
+  val pattern: term -> bool
 end;
 
 structure Pattern: PATTERN =
@@ -375,5 +376,12 @@
   val envir' = apfst (typ_match thy (pT, oT)) envir;
 in mtch [] po envir' handle Pattern => first_order_match thy po envir' end;
 
+
+fun pattern (Abs (_, _, t)) = pattern t
+  | pattern t =
+      let val (head, args) = strip_comb t in
+        if is_Var head then
+          forall is_Bound args andalso not (has_duplicates (op aconv) args)
+        else forall pattern args
+      end;
 end;
-