src/Pure/raw_simplifier.ML
changeset 61090 16f7f9aa4263
parent 61057 5f6a1e31f3ad
child 61095 50e793295ce1
     1.1 --- a/src/Pure/raw_simplifier.ML	Wed Sep 02 19:53:49 2015 +0200
     1.2 +++ b/src/Pure/raw_simplifier.ML	Wed Sep 02 20:14:19 2015 +0200
     1.3 @@ -577,11 +577,15 @@
     1.4  
     1.5  (* add/del rules explicitly *)
     1.6  
     1.7 +local
     1.8 +
     1.9  fun comb_simps ctxt comb mk_rrule thms =
    1.10    let
    1.11 -    val rews = extract_rews ctxt thms;
    1.12 +    val rews = extract_rews ctxt (map (Thm.transfer (Proof_Context.theory_of ctxt)) thms);
    1.13    in fold (fold comb o mk_rrule) rews ctxt end;
    1.14  
    1.15 +in
    1.16 +
    1.17  fun ctxt addsimps thms =
    1.18    comb_simps ctxt insert_rrule (mk_rrule ctxt) thms;
    1.19  
    1.20 @@ -591,6 +595,8 @@
    1.21  fun add_simp thm ctxt = ctxt addsimps [thm];
    1.22  fun del_simp thm ctxt = ctxt delsimps [thm];
    1.23  
    1.24 +end;
    1.25 +
    1.26  
    1.27  (* congs *)
    1.28