# 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 *)