--- a/src/Provers/splitter.ML Sat Nov 02 21:42:45 2019 +0000
+++ b/src/Provers/splitter.ML Sun Nov 03 10:29:01 2019 +0000
@@ -98,7 +98,7 @@
val meta_iffD = Data.meta_eq_to_iff RS Data.iffD; (* (P == Q) ==> Q ==> P *)
-val lift = Goal.prove_global \<^theory>\<open>Pure\<close> ["P", "Q", "R"]
+val lift = Goal.prove_global \<^theory> ["P", "Q", "R"]
[Syntax.read_prop_global \<^theory>\<open>Pure\<close> "!!x :: 'b. Q(x) == R(x) :: 'c"]
(Syntax.read_prop_global \<^theory>\<open>Pure\<close> "P(%x. Q(x)) == P(%x. R(x))")
(fn {context = ctxt, prems} =>
--- a/src/Pure/global_theory.ML Sat Nov 02 21:42:45 2019 +0000
+++ b/src/Pure/global_theory.ML Sun Nov 03 10:29:01 2019 +0000
@@ -291,10 +291,7 @@
if Binding.is_empty b then
let
val (thms, thy') = app_facts facts thy;
- val _ =
- if Proofterm.export_proof_boxes_required thy' then
- Proofterm.export_proof_boxes (map Thm.proof_of thms)
- else ();
+ val _ = Thm.expose_proofs thy' thms;
in register_proofs thms thy' end
else
let
--- a/src/Pure/more_thm.ML Sat Nov 02 21:42:45 2019 +0000
+++ b/src/Pure/more_thm.ML Sun Nov 03 10:29:01 2019 +0000
@@ -113,6 +113,7 @@
val tag: string * string -> attribute
val untag: string -> attribute
val kind: string -> attribute
+ val expose_proofs: theory -> thm list -> unit
val reconstruct_proof_of: thm -> Proofterm.proof
val standard_proof_of: {full: bool, expand_name: Proofterm.thm_header -> string option} ->
thm -> Proofterm.proof
@@ -654,6 +655,11 @@
(** proof terms **)
+fun expose_proofs thy thms =
+ if Proofterm.export_proof_boxes_required thy then
+ Proofterm.export_proof_boxes (map Thm.proof_of thms)
+ else ();
+
fun reconstruct_proof_of thm =
Proofterm.reconstruct_proof (Thm.theory_of_thm thm) (Thm.prop_of thm) (Thm.proof_of thm);