# HG changeset patch
# User wenzelm
# Date 878726107 -3600
# Node ID d182dc0a34f6b0e6d623474ee40455d77830ffcc
# Parent  b76a494908332640b3b233ad1b633821f11f6b1e
fixed exception OPTION;

diff -r b76a49490833 -r d182dc0a34f6 src/Pure/type.ML
--- a/src/Pure/type.ML	Wed Nov 05 11:34:44 1997 +0100
+++ b/src/Pure/type.ML	Wed Nov 05 11:35:07 1997 +0100
@@ -112,11 +112,11 @@
 
 fun freezeOne alist (ix,sort) =
   TFree (the (assoc (alist, ix)), sort)
-    handle OPTION _ =>
+    handle OPTION =>
       raise TYPE ("Failure during freezing of ?" ^ string_of_indexname ix, [], []);
 
 fun thawOne alist (a,sort) = TVar (the (assoc (alist,a)), sort)
-      handle OPTION _ => TFree(a,sort);
+      handle OPTION => TFree(a,sort);
 
 (*This sort of code could replace unvarifyT (?)
     fun freeze_thaw_type T =