changeset 5342 | 3be51e9b33c8 |
parent 4999 | 4c74267cfa0c |
child 5344 | 6a949382cdfe |
--- a/src/Pure/thm.ML Wed Aug 19 10:37:07 1998 +0200 +++ b/src/Pure/thm.ML Wed Aug 19 10:37:56 1998 +0200 @@ -1889,7 +1889,7 @@ lhs, elhs, fo, perm} = let val _ = if Sign.subsig (Sign.deref sign_ref, signt) then () - else (trace_thm true "Rewrite rule from different theory:" thm; + else (prthm true "Rewrite rule from different theory:" thm; raise Pattern.MATCH); val rprop = if maxt = ~1 then prop else Logic.incr_indexes([],maxt+1) prop;