Mercurial Mercurial > repos > isabelle / changeset
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | raw | gz | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
tuned msg;
authorwenzelm
Mon, 08 May 2000 11:45:57 +0200
changeset 8831 b824c0c55613
parent 8830 3e95f3a90875
child 8832 bcceda950cd0
tuned msg;
src/Pure/thm.ML file | annotate | diff | comparison | revisions 
--- a/src/Pure/thm.ML	Mon May 08 11:45:47 2000 +0200
+++ b/src/Pure/thm.ML	Mon May 08 11:45:57 2000 +0200
@@ -2030,7 +2030,7 @@
             lhs, elhs, fo, perm} =
       let
         val _ = if Sign.subsig (Sign.deref sign_ref, signt) then ()
-                else (prthm true "Rewrite rule from different theory:" thm;
+                else (prthm true "Ignoring rewrite rule from different theory:" thm;
                       raise Pattern.MATCH);
         val rprop = if maxt = ~1 then prop
                     else Logic.incr_indexes([],maxt+1) prop;
isabelle