1.1 --- a/src/Pure/meta_simplifier.ML	Mon Jan 24 18:09:29 2005 +0100
     1.2 +++ b/src/Pure/meta_simplifier.ML	Mon Jan 24 18:11:06 2005 +0100
     1.3 @@ -792,9 +792,6 @@
     1.4      fun rew {thm, name, lhs, elhs, fo, perm} =
     1.5        let
     1.6          val {sign, prop, maxidx, ...} = rep_thm thm;
     1.7 -        val _ = if Sign.subsig (sign, signt) then ()
     1.8 -                else (warn_thm "Ignoring rewrite rule from different theory:" thm;
     1.9 -                      raise Pattern.MATCH);
    1.10          val (rthm, elhs') = if maxt = ~1 then (thm, elhs)
    1.11            else (Thm.incr_indexes (maxt+1) thm, Thm.cterm_incr_indexes (maxt+1) elhs);
    1.12          val insts = if fo then Thm.cterm_first_order_match (elhs', eta_t')
    1.13 @@ -872,8 +869,6 @@
    1.14  
    1.15  fun congc (prover,signt,maxt) {thm=cong,lhs=lhs} t =
    1.16    let val sign = Thm.sign_of_thm cong
    1.17 -      val _ = if Sign.subsig (sign, signt) then ()
    1.18 -                 else error("Congruence rule from different theory")
    1.19        val rthm = if maxt = ~1 then cong else Thm.incr_indexes (maxt+1) cong;
    1.20        val rlhs = fst (Drule.dest_equals (Drule.strip_imp_concl (cprop_of rthm)));
    1.21        val insts = Thm.cterm_match (rlhs, t)