# HG changeset patch
# User paulson
# Date 1572776941 0
# Node ID bb403cb94db25cc94a373c82ddd37584038313e0
# Parent  15129c2f4a333fa3808254c28553888edf79094f# Parent  e892f7a1fd83a35a04169a3c781e1ab3b6cda314
merged

diff -r e892f7a1fd83 -r bb403cb94db2 src/Provers/splitter.ML
--- 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} =>
diff -r e892f7a1fd83 -r bb403cb94db2 src/Pure/global_theory.ML
--- 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
diff -r e892f7a1fd83 -r bb403cb94db2 src/Pure/more_thm.ML
--- 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);