diff -r 507c65cc4332 -r f244926013e5 src/Pure/term.ML
--- 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 *)