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;