Symtab.lookup_multi;

--- a/src/Pure/term.ML	Sat Jul 10 21:40:14 1999 +0200
+++ b/src/Pure/term.ML	Sat Jul 10 21:41:05 1999 +0200
@@ -985,8 +985,7 @@
 
 fun compress_type T =
   let val tag = type_tag T
-      val tylist = the (Symtab.lookup (!memo_types, tag))
-	           handle _ => []
+      val tylist = Symtab.lookup_multi (!memo_types, tag)
   in  
       case find_type (T,tylist) of
 	Some T' => T'
@@ -1022,8 +1021,7 @@
   | share_term (Abs (a,T,u)) = Abs (a, T, share_term u)
   | share_term t =
       let val tag = const_tag t
-	  val ts = the (Symtab.lookup (!memo_terms, tag))
-	               handle _ => []
+	  val ts = Symtab.lookup_multi (!memo_terms, tag)
       in 
 	  case find_term (t,ts) of
 	      Some t' => t'