--- a/src/Doc/Implementation/Proof.thy Sat May 20 17:18:44 2023 +0200
+++ b/src/Doc/Implementation/Proof.thy Sat May 20 17:42:01 2023 +0200
@@ -270,7 +270,7 @@
cterm list -> Proof.context -> thm list * Proof.context"} \\
@{define_ML Assumption.add_assumes: "
cterm list -> Proof.context -> thm list * Proof.context"} \\
- @{define_ML Assumption.export: "bool -> Proof.context -> Proof.context -> thm -> thm"} \\
+ @{define_ML Assumption.export: "Proof.context -> Proof.context -> thm -> thm"} \\
@{define_ML Assumption.export_term: "Proof.context -> Proof.context -> term -> term"} \\
\end{mldecls}
@@ -290,9 +290,9 @@
\<^ML>\<open>Assumption.add_assms\<close> where the export rule performs \<open>\<Longrightarrow>\<hyphen>intro\<close> or
\<open>#\<Longrightarrow>\<hyphen>intro\<close>, depending on goal mode.
- \<^descr> \<^ML>\<open>Assumption.export\<close>~\<open>is_goal inner outer thm\<close> exports result \<open>thm\<close>
- from the \<open>inner\<close> context back into the \<open>outer\<close> one; \<open>is_goal = true\<close> means
- this is a goal context. The result is in HHF normal form. Note that
+ \<^descr> \<^ML>\<open>Assumption.export\<close>~\<open>inner outer thm\<close> exports result \<open>thm\<close> from the
+ \<open>inner\<close> context back into the \<open>outer\<close> one; \<^ML>\<open>Assumption.export_goal\<close>
+ does the same in a goal context. The result is in HHF normal form. Note that
\<^ML>\<open>Proof_Context.export\<close> combines \<^ML>\<open>Variable.export\<close> and
\<^ML>\<open>Assumption.export\<close> in the canonical way.
@@ -318,7 +318,7 @@
val eq' = Thm.symmetric eq;
(*back to original context -- discharges assumption*)
- val r = Assumption.export false ctxt1 ctxt0 eq';
+ val r = Assumption.export ctxt1 ctxt0 eq';
\<close>
text \<open>
--- a/src/Pure/Isar/local_defs.ML Sat May 20 17:18:44 2023 +0200
+++ b/src/Pure/Isar/local_defs.ML Sat May 20 17:42:01 2023 +0200
@@ -155,7 +155,7 @@
if t aconv u then (asm, false)
else (Drule.abs_def (Variable.gen_all outer asm), true))
end)));
- in (apply2 (map #1) (List.partition #2 defs_asms), Assumption.export false inner outer th) end;
+ in (apply2 (map #1) (List.partition #2 defs_asms), Assumption.export inner outer th) end;
(*
[xs, xs \<equiv> as]
--- a/src/Pure/Isar/proof.ML Sat May 20 17:18:44 2023 +0200
+++ b/src/Pure/Isar/proof.ML Sat May 20 17:42:01 2023 +0200
@@ -477,7 +477,7 @@
in
result
|> map (Raw_Simplifier.norm_hhf result_ctxt #> protect_prems)
- |> Proof_Context.goal_export result_ctxt goal_ctxt
+ |> Proof_Context.export_goal result_ctxt goal_ctxt
|> (fn rules => Seq.lift provide_goal (EVERY (map refine rules) goal) state)
end;
@@ -1096,7 +1096,7 @@
let
val ctxt' = context_of state';
val export0 =
- Assumption.export false result_ctxt (Proof_Context.augment result_text ctxt') #>
+ Assumption.export result_ctxt (Proof_Context.augment result_text ctxt') #>
fold_rev (fn (x, v) => Thm.forall_intr_name (x, Thm.cterm_of params_ctxt v)) params #>
Raw_Simplifier.norm_hhf_protect ctxt';
val export = map export0 #> Variable.export result_ctxt ctxt';
--- a/src/Pure/Isar/proof_context.ML Sat May 20 17:18:44 2023 +0200
+++ b/src/Pure/Isar/proof_context.ML Sat May 20 17:42:01 2023 +0200
@@ -102,8 +102,9 @@
val standard_typ_check: Proof.context -> typ list -> typ list
val standard_term_check_finish: Proof.context -> term list -> term list
val standard_term_uncheck: Proof.context -> term list -> term list
- val goal_export: Proof.context -> Proof.context -> thm list -> thm list
+ val export_: {goal: bool} -> Proof.context -> Proof.context -> thm list -> thm list
val export: Proof.context -> Proof.context -> thm list -> thm list
+ val export_goal: Proof.context -> Proof.context -> thm list -> thm list
val export_morphism: Proof.context -> Proof.context -> morphism
val auto_bind_goal: term list -> Proof.context -> Proof.context
val auto_bind_facts: term list -> Proof.context -> Proof.context
@@ -838,12 +839,12 @@
(** export results **)
-fun common_export is_goal inner outer =
- map (Assumption.export is_goal inner outer) #>
+fun export_ goal inner outer =
+ map (Assumption.export_ goal inner outer) #>
Variable.export inner outer;
-val goal_export = common_export true;
-val export = common_export false;
+val export = export_{goal = false};
+val export_goal = export_{goal = true};
fun export_morphism inner outer =
Assumption.export_morphism inner outer $>
--- a/src/Pure/assumption.ML Sat May 20 17:18:44 2023 +0200
+++ b/src/Pure/assumption.ML Sat May 20 17:42:01 2023 +0200
@@ -18,7 +18,9 @@
val add_assms: export -> cterm list -> Proof.context -> thm list * Proof.context
val add_assumes: cterm list -> Proof.context -> thm list * Proof.context
val export_term: Proof.context -> Proof.context -> term -> term
- val export: bool -> Proof.context -> Proof.context -> thm -> thm
+ val export_: {goal: bool} -> Proof.context -> Proof.context -> thm -> thm
+ val export: Proof.context -> Proof.context -> thm -> thm
+ val export_goal: Proof.context -> Proof.context -> thm -> thm
val export_morphism: Proof.context -> Proof.context -> morphism
end;
@@ -134,11 +136,14 @@
fun export_thm is_goal inner outer =
fold_rev (fn (e, As) => #1 (e is_goal As)) (local_assumptions_of inner outer);
-fun export is_goal inner outer =
+fun export_{goal} inner outer =
Raw_Simplifier.norm_hhf_protect inner #>
- export_thm is_goal inner outer #>
+ export_thm goal inner outer #>
Raw_Simplifier.norm_hhf_protect outer;
+val export = export_{goal = false};
+val export_goal = export_{goal = true};
+
fun export_morphism inner outer =
let
val export0 = export_thm false inner outer;
--- a/src/Pure/goal.ML Sat May 20 17:18:44 2023 +0200
+++ b/src/Pure/goal.ML Sat May 20 17:42:01 2023 +0200
@@ -221,7 +221,7 @@
res
|> Thm.close_derivation \<^here>
|> Conjunction.elim_balanced (length props)
- |> map (Assumption.export false ctxt' ctxt)
+ |> map (Assumption.export ctxt' ctxt)
|> Variable.export ctxt' ctxt
|> map Drule.zero_var_indexes
end;