# HG changeset patch
# User wenzelm
# Date 1441217659 -7200
# Node ID 16f7f9aa4263b38ec0838ff1ec7a12ae7011b078
# Parent  969eb24297afe766d01849fdb26ce903526a5526
more thorough transfer;

diff -r 969eb24297af -r 16f7f9aa4263 src/Pure/raw_simplifier.ML
--- a/src/Pure/raw_simplifier.ML	Wed Sep 02 19:53:49 2015 +0200
+++ b/src/Pure/raw_simplifier.ML	Wed Sep 02 20:14:19 2015 +0200
@@ -577,11 +577,15 @@
 
 (* add/del rules explicitly *)
 
+local
+
 fun comb_simps ctxt comb mk_rrule thms =
   let
-    val rews = extract_rews ctxt thms;
+    val rews = extract_rews ctxt (map (Thm.transfer (Proof_Context.theory_of ctxt)) thms);
   in fold (fold comb o mk_rrule) rews ctxt end;
 
+in
+
 fun ctxt addsimps thms =
   comb_simps ctxt insert_rrule (mk_rrule ctxt) thms;
 
@@ -591,6 +595,8 @@
 fun add_simp thm ctxt = ctxt addsimps [thm];
 fun del_simp thm ctxt = ctxt delsimps [thm];
 
+end;
+
 
 (* congs *)