src/Pure/net.ML

             Net{comb=ins1(keys,comb), var=var, atoms=atoms}
         | ins1 (VarK :: keys, Net{comb,var,atoms}) =
             Net{comb=comb, var=ins1(keys,var), atoms=atoms}
         | ins1 (AtomK a :: keys, Net{comb,var,atoms}) =
             let
-              val net' = if_none (Symtab.lookup atoms a) empty;
+              val net' = the_default empty (Symtab.lookup atoms a);
               val atoms' = Symtab.update (a, ins1 (keys, net')) atoms;
             in  Net{comb=comb, var=var, atoms=atoms'}  end
   in  ins1 (keys,net)  end;
 
 fun insert_safe eq entry net = insert eq entry net handle INSERT => net;

       | subtr (Net {comb = comb1, var = var1, atoms = atoms1})
             (Net {comb = comb2, var = var2, atoms = atoms2}) =
           subtr comb1 comb2
           #> subtr var1 var2
           #> Symtab.fold (fn (a, net) =>
-            subtr (if_none (Symtab.lookup atoms1 a) emptynet) net) atoms2
+            subtr (the_default emptynet (Symtab.lookup atoms1 a)) net) atoms2
   in subtr net1 net2 [] end;
 
 fun entries net = subtract (K false) empty net;