# HG changeset patch
# User wenzelm
# Date 876155383 -7200
# Node ID ec519ba6196ebb0c68063f90b6a27eefcac46b4a
# Parent  ac23a9ab3cd648452f6934a949f5d4b2f7206920
eliminated raise_term;

diff -r ac23a9ab3cd6 -r ec519ba6196e src/Pure/term.ML
--- a/src/Pure/term.ML	Mon Oct 06 18:29:11 1997 +0200
+++ b/src/Pure/term.ML	Mon Oct 06 18:29:43 1997 +0200
@@ -56,13 +56,9 @@
 (*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