# HG changeset patch
# User wenzelm
# Date 1518805853 -3600
# Node ID b7d90c4a3897ffbc0622b692ac94a976a229874e
# Parent  25cb2299f8a4fbe937c335771b3019432c733a3f
trim context of persistent data;
tuned;

diff -r 25cb2299f8a4 -r b7d90c4a3897 src/HOL/Tools/lin_arith.ML
--- a/src/HOL/Tools/lin_arith.ML	Fri Feb 16 19:30:28 2018 +0100
+++ b/src/HOL/Tools/lin_arith.ML	Fri Feb 16 19:30:53 2018 +0100
@@ -85,8 +85,12 @@
 
 val get_arith_data = Lin_Arith_Data.get o Context.Proof;
 
+fun get_splits ctxt =
+  #splits (get_arith_data ctxt)
+  |> map (Thm.transfer (Proof_Context.theory_of ctxt));
+
 fun add_split thm = Lin_Arith_Data.map (fn {splits, inj_consts, discrete} =>
-  {splits = update Thm.eq_thm_prop thm splits,
+  {splits = update Thm.eq_thm_prop (Thm.trim_context thm) splits,
    inj_consts = inj_consts, discrete = discrete});
 
 fun add_discrete_type d = Lin_Arith_Data.map (fn {splits, inj_consts, discrete} =>
@@ -418,7 +422,7 @@
   (* where ti' = HOLogic.dest_Trueprop ti                                    *)
   fun REPEAT_DETERM_etac_rev_mp tms =
     fold (curry HOLogic.mk_imp) (map HOLogic.dest_Trueprop tms) \<^term>\<open>False\<close>
-  val split_thms  = filter (is_split_thm ctxt) (#splits (get_arith_data ctxt))
+  val split_thms  = filter (is_split_thm ctxt) (get_splits ctxt)
   val cmap        = Splitter.cmap_of_split_thms split_thms
   val goal_tm     = REPEAT_DETERM_etac_rev_mp terms
   val splits      = Splitter.split_posns cmap thy Ts goal_tm
@@ -819,7 +823,7 @@
 
 fun pre_tac ctxt i =
   let
-    val split_thms = filter (is_split_thm ctxt) (#splits (get_arith_data ctxt))
+    val split_thms = filter (is_split_thm ctxt) (get_splits ctxt)
     fun is_relevant t = is_some (decomp ctxt t)
   in
     DETERM (
@@ -940,7 +944,7 @@
     (* split_limit may trigger.                                           *)
     (* Therefore splitting outside of simple_tac may allow us to prove    *)
     (* some goals that simple_tac alone would fail on.                    *)
-    (REPEAT_DETERM o split_tac ctxt (#splits (get_arith_data ctxt)))
+    (REPEAT_DETERM o split_tac ctxt (get_splits ctxt))
     (Fast_Arith.lin_arith_tac ctxt);
 
 in