added raise_type: string -> typ list -> term list -> 'a;
added raise_term: string -> term list -> 'a;
--- 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