# HG changeset patch
# User wenzelm
# Date 750079997 -3600
# Node ID 3f9f8395519e88de2ac3740ac5f15b3605fb9e11
# Parent  deb04a336a99f3857520526fb752a80727034301
added raise_type: string -> typ list -> term list -> 'a;
added raise_term: string -> term list -> 'a;

diff -r deb04a336a99 -r 3f9f8395519e src/Pure/term.ML
--- a/src/Pure/term.ML	Fri Oct 08 12:30:01 1993 +0100
+++ b/src/Pure/term.ML	Fri Oct 08 12:33:17 1993 +0100
@@ -52,9 +52,13 @@
 (*For errors involving type mismatches*)
 exception TYPE of string * typ list * term list;
 
+fun raise_type msg tys ts = raise TYPE (msg, tys, ts);
+
 (*For system errors involving terms*)
 exception TERM of string * term list;
 
+fun raise_term msg ts = raise TERM (msg, ts);
+
 
 (*Note variable naming conventions!
     a,b,c: string