# HG changeset patch
# User wenzelm
# Date 1470421047 -7200
# Node ID 676ba20db06335c2ac485a14266c5e1e9a87b51a
# Parent  1555dc12cfb6c2711973e46f9840e5940d973da8
tuned;

diff -r 1555dc12cfb6 -r 676ba20db063 src/Pure/net.ML
--- a/src/Pure/net.ML	Fri Aug 05 18:14:34 2016 +0200
+++ b/src/Pure/net.ML	Fri Aug 05 20:17:27 2016 +0200
@@ -154,20 +154,15 @@
 
 (*** Retrieval functions for discrimination nets ***)
 
-exception ABSENT;
-
-fun the_atom atoms a =
-  (case Symtab.lookup atoms a of
-    NONE => raise ABSENT
-  | SOME net => net);
-
 (*Return the list of items at the given node, [] if no such node*)
 fun lookup (Leaf xs) [] = xs
   | lookup (Leaf _) (_ :: _) = []  (*non-empty keys and empty net*)
-  | lookup (Net {comb, var, atoms}) (CombK :: keys) = lookup comb keys
-  | lookup (Net {comb, var, atoms}) (VarK :: keys) = lookup var keys
-  | lookup (Net {comb, var, atoms}) (AtomK a :: keys) =
-      lookup (the_atom atoms a) keys handle ABSENT => [];
+  | lookup (Net {comb, ...}) (CombK :: keys) = lookup comb keys
+  | lookup (Net {var, ...}) (VarK :: keys) = lookup var keys
+  | lookup (Net {atoms, ...}) (AtomK a :: keys) =
+      (case Symtab.lookup atoms a of
+        SOME net => lookup net keys
+      | NONE => []);
 
 
 (*Skipping a term in a net.  Recursively skip 2 levels if a combination*)
@@ -180,7 +175,9 @@
 
 (*conses the linked net, if present, to nets*)
 fun look1 (atoms, a) nets =
-  the_atom atoms a :: nets handle ABSENT => nets;
+  (case Symtab.lookup atoms a of
+    NONE => nets
+  | SOME net => net :: nets);
 
 (*Return the nodes accessible from the term (cons them before nets)
   "unif" signifies retrieval for unification rather than matching.