--- a/src/Pure/goal.ML Fri Oct 15 21:59:46 2021 +0200
+++ b/src/Pure/goal.ML Fri Oct 15 22:00:28 2021 +0200
@@ -24,23 +24,22 @@
val norm_result: Proof.context -> thm -> thm
val skip_proofs_enabled: unit -> bool
val future_result: Proof.context -> thm future -> term -> thm
- type goal_context = {prems: thm list, context: Proof.context}
- val prove_internal: Proof.context -> cterm list -> cterm -> (goal_context -> tactic) -> 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 ->
- (goal_context -> tactic) -> thm list
+ ({prems: thm list, context: Proof.context} -> tactic) -> thm list
val prove_future: Proof.context -> string list -> term list -> term ->
- (goal_context -> tactic) -> thm
+ ({prems: thm list, context: Proof.context} -> tactic) -> thm
val prove: Proof.context -> string list -> term list -> term ->
- (goal_context -> tactic) -> thm
+ ({prems: thm list, context: Proof.context} -> tactic) -> thm
val prove_global_future: theory -> string list -> term list -> term ->
- (goal_context -> tactic) -> thm
+ ({prems: thm list, context: Proof.context} -> tactic) -> thm
val prove_global: theory -> string list -> term list -> term ->
- (goal_context -> tactic) -> thm
+ ({prems: thm list, context: Proof.context} -> tactic) -> thm
val prove_sorry: Proof.context -> string list -> term list -> term ->
- (goal_context -> tactic) -> thm
+ ({prems: thm list, context: Proof.context} -> tactic) -> thm
val prove_sorry_global: theory -> string list -> term list -> term ->
- (goal_context -> tactic) -> thm
+ ({prems: thm list, context: Proof.context} -> tactic) -> thm
val restrict: int -> int -> thm -> thm
val unrestrict: int -> thm -> thm
val conjunction_tac: int -> tactic
@@ -153,21 +152,12 @@
(** tactical theorem proving **)
-type goal_context = {prems: thm list, context: Proof.context};
-
-
(* prove_internal -- minimal checks, no normalization of result! *)
fun prove_internal ctxt casms cprop tac =
- let
- val (prems, ctxt') = ctxt
- |> fold (Variable.declare_term o Thm.term_of) (casms @ [cprop])
- |> fold_map Thm.assume_hyps casms;
- in
- (case SINGLE (tac {prems = prems, context = ctxt'}) (init cprop) of
- SOME th => Drule.implies_intr_list casms (finish ctxt' th)
- | NONE => error "Tactic failed")
- end;
+ (case SINGLE (tac (map (Assumption.assume ctxt) casms)) (init cprop) of
+ SOME th => Drule.implies_intr_list casms (finish ctxt th)
+ | NONE => error "Tactic failed");
(* prove variations *)