--- 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} =>