--- a/src/Pure/term.ML Sat Sep 03 17:20:35 2022 +0200
+++ b/src/Pure/term.ML Sat Sep 03 17:37:46 2022 +0200
@@ -114,6 +114,7 @@
val exists_type: (typ -> bool) -> term -> bool
val exists_subterm: (term -> bool) -> term -> bool
val exists_Const: (string * typ -> bool) -> term -> bool
+ val is_schematic: term -> bool
end;
signature TERM =
@@ -950,6 +951,10 @@
fun exists_Const P = exists_subterm (fn Const c => P c | _ => false);
+fun is_schematic t =
+ exists_subterm is_Var t orelse
+ (exists_type o exists_subtype) is_TVar t;
+
(* contraction *)