# HG changeset patch
# User wenzelm
# Date 1518885255 -3600
# Node ID 15c6256709d68125c529ff329eadeeff272ddb5a
# Parent  b846f7a11fda5b63b2687c6f0edc0d7ede3cfe41
trim context of persistent data;

diff -r b846f7a11fda -r 15c6256709d6 src/Provers/splitter.ML
--- a/src/Provers/splitter.ML	Sat Feb 17 16:42:15 2018 +0100
+++ b/src/Provers/splitter.ML	Sat Feb 17 17:34:15 2018 +0100
@@ -438,12 +438,15 @@
 fun gen_add_split bang split ctxt =
   let
     val (name, asm) = split_thm_info split
+    val split0 = Thm.trim_context split
     fun tac ctxt' =
-      (if asm then split_asm_tac ctxt' [split]
-       else if bang
-            then split_tac ctxt' [split] THEN_ALL_NEW
-                 TRY o (SELECT_GOAL (Data.safe_tac ctxt'))
-            else split_tac ctxt' [split])
+      let val split' = Thm.transfer (Proof_Context.theory_of ctxt') split0 in
+        (if asm then split_asm_tac ctxt' [split']
+         else if bang
+              then split_tac ctxt' [split'] THEN_ALL_NEW
+                   TRY o (SELECT_GOAL (Data.safe_tac ctxt'))
+              else split_tac ctxt' [split'])
+      end
   in Simplifier.addloop (ctxt, (split_name name asm, tac)) end;
 
 val add_split = gen_add_split false;