# HG changeset patch
# User wenzelm
# Date 1565166714 -7200
# Node ID 94ed5be08e7fec592ac7ef37ea83ffa41c745e79
# Parent  90acc6ce5bebe75d7bac6bdcfda373f9728f96cb
more careful treatment of implicit context;

diff -r 90acc6ce5beb -r 94ed5be08e7f src/FOLP/simp.ML
--- a/src/FOLP/simp.ML	Wed Aug 07 09:28:32 2019 +0200
+++ b/src/FOLP/simp.ML	Wed Aug 07 10:31:54 2019 +0200
@@ -255,13 +255,13 @@
 val insert_thms = fold_rev insert_thm;
 
 fun addrew ctxt thm (SS{auto_tac,congs,cong_net,mk_simps,simps,simp_net}) =
-let val thms = mk_simps ctxt thm
+let val thms = map Thm.trim_context (mk_simps ctxt thm)
 in SS{auto_tac=auto_tac,congs=congs, cong_net=cong_net, mk_simps=mk_simps,
       simps = (thm,thms)::simps, simp_net = insert_thms thms simp_net}
 end;
 
 fun op addcongs(SS{auto_tac,congs,cong_net,mk_simps,simps,simp_net}, thms) =
-let val congs' = thms @ congs;
+let val congs' = map Thm.trim_context thms @ congs;
 in SS{auto_tac=auto_tac, congs= congs',
       cong_net= insert_thms (map mk_trans thms) cong_net,
       mk_simps = fn ctxt => normed_rews ctxt congs', simps=simps, simp_net=simp_net}