summary |
shortlog |
changelog |
graph |
tags |
bookmarks |
branches |
files |
changeset |
raw | gz |
help

author | paulson |

Wed, 19 Aug 1998 10:37:56 +0200 | |

changeset 5342 | 3be51e9b33c8 |

parent 5341 | eb105c6931a4 |

child 5343 | 871b77df79a0 |

The warning "Rewrite rule from different theory" is ALWAYS printed, even if
tracing is off.

src/Pure/thm.ML | file | annotate | diff | comparison | revisions |

--- 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;