# HG changeset patch
# User wenzelm
# Date 1572734588 -3600
# Node ID 15129c2f4a333fa3808254c28553888edf79094f
# Parent  41685289b8eb7451ee5ae0e72f342235ab70d3f5
proper theory for export_proofs;

diff -r 41685289b8eb -r 15129c2f4a33 src/Provers/splitter.ML
--- a/src/Provers/splitter.ML	Sat Nov 02 23:13:15 2019 +0100
+++ b/src/Provers/splitter.ML	Sat Nov 02 23:43:08 2019 +0100
@@ -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} =>