--- 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 *)