# HG changeset patch
# User berghofe
# Date 1106586666 -3600
# Node ID dd48bf51aff196f2c98db9a235ad73375dda3841
# Parent  16dd63c7804931a0578c34a8dea40f0c7e9c05f1
Removed unnecessary subsignature checks to speed up rewriting.

diff -r 16dd63c78049 -r dd48bf51aff1 src/Pure/meta_simplifier.ML
--- a/src/Pure/meta_simplifier.ML	Mon Jan 24 18:09:29 2005 +0100
+++ b/src/Pure/meta_simplifier.ML	Mon Jan 24 18:11:06 2005 +0100
@@ -792,9 +792,6 @@
     fun rew {thm, name, lhs, elhs, fo, perm} =
       let
         val {sign, prop, maxidx, ...} = rep_thm thm;
-        val _ = if Sign.subsig (sign, signt) then ()
-                else (warn_thm "Ignoring rewrite rule from different theory:" thm;
-                      raise Pattern.MATCH);
         val (rthm, elhs') = if maxt = ~1 then (thm, elhs)
           else (Thm.incr_indexes (maxt+1) thm, Thm.cterm_incr_indexes (maxt+1) elhs);
         val insts = if fo then Thm.cterm_first_order_match (elhs', eta_t')
@@ -872,8 +869,6 @@
 
 fun congc (prover,signt,maxt) {thm=cong,lhs=lhs} t =
   let val sign = Thm.sign_of_thm cong
-      val _ = if Sign.subsig (sign, signt) then ()
-                 else error("Congruence rule from different theory")
       val rthm = if maxt = ~1 then cong else Thm.incr_indexes (maxt+1) cong;
       val rlhs = fst (Drule.dest_equals (Drule.strip_imp_concl (cprop_of rthm)));
       val insts = Thm.cterm_match (rlhs, t)