# HG changeset patch
# User wenzelm
# Date 878385421 -3600
# Node ID edd8cb346109209cf76f554c0abc6b8230fa627b
# Parent  abb0f4742ed7b8888d959aafbb49bc9bf7c48abe
propagate exn msg;

diff -r abb0f4742ed7 -r edd8cb346109 src/Pure/drule.ML
--- a/src/Pure/drule.ML	Fri Oct 31 15:28:01 1997 +0100
+++ b/src/Pure/drule.ML	Sat Nov 01 12:57:01 1997 +0100
@@ -329,7 +329,7 @@
   in  instantiate (map ctyp2 tye, map instT ctpairs0) th  end
   handle TERM _ =>
            raise THM("cterm_instantiate: incompatible signatures",0,[th])
-       | TYPE _ => raise THM("cterm_instantiate: types", 0, [th])
+       | TYPE (msg, _, _) => raise THM("cterm_instantiate: " ^ msg, 0, [th])
 end;