# HG changeset patch
# User wenzelm
# Date 1662219466 -7200
# Node ID f244926013e5aeda232d3f7594634528debcbaa6
# Parent  507c65cc4332d345a3978d0b4c36b7cd30c370d8
tuned signature;

diff -r 507c65cc4332 -r f244926013e5 src/Pure/Isar/proof.ML
--- a/src/Pure/Isar/proof.ML	Sat Sep 03 17:20:35 2022 +0200
+++ b/src/Pure/Isar/proof.ML	Sat Sep 03 17:37:46 2022 +0200
@@ -1147,13 +1147,13 @@
 
 fun schematic_goal state =
   let val (_, {statement = (_, _, prop), ...}) = find_goal state
-  in Goal.is_schematic prop end;
+  in Term.is_schematic prop end;
 
 fun is_relevant state =
   (case try find_goal state of
     NONE => true
   | SOME (_, {statement = (_, _, prop), goal, ...}) =>
-      Goal.is_schematic prop orelse not (Logic.protect prop aconv Thm.concl_of goal));
+      Term.is_schematic prop orelse not (Logic.protect prop aconv Thm.concl_of goal));
 
 
 (* terminal proof steps *)
diff -r 507c65cc4332 -r f244926013e5 src/Pure/goal.ML
--- a/src/Pure/goal.ML	Sat Sep 03 17:20:35 2022 +0200
+++ b/src/Pure/goal.ML	Sat Sep 03 17:37:46 2022 +0200
@@ -25,7 +25,6 @@
   val skip_proofs_enabled: unit -> bool
   val future_result: Proof.context -> thm future -> term -> thm
   val prove_internal: Proof.context -> cterm list -> cterm -> (thm list -> tactic) -> thm
-  val is_schematic: term -> bool
   val prove_common: Proof.context -> int option -> string list -> term list -> term list ->
     ({prems: thm list, context: Proof.context} -> tactic) -> thm list
   val prove_future: Proof.context -> string list -> term list -> term ->
@@ -162,15 +161,11 @@
 
 (* prove variations *)
 
-fun is_schematic t =
-  Term.exists_subterm Term.is_Var t orelse
-  Term.exists_type (Term.exists_subtype Term.is_TVar) t;
-
 fun prove_common ctxt fork_pri xs asms props tac =
   let
     val thy = Proof_Context.theory_of ctxt;
 
-    val schematic = exists is_schematic props;
+    val schematic = exists Term.is_schematic props;
     val immediate = is_none fork_pri;
     val future = Future.proofs_enabled 1 andalso not (Proofterm.proofs_enabled ());
     val skip = not immediate andalso not schematic andalso future andalso skip_proofs_enabled ();
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 *)