src/Pure/net.ML

 *)
 fun add_key_of_terms (t, cs) =
   let fun rands (f$t, cs) = CombK :: rands (f, add_key_of_terms(t, cs))
         | rands (Const(c,_), cs) = AtomK c :: cs
         | rands (Free(c,_),  cs) = AtomK c :: cs
-        | rands (Bound i,  cs)   = AtomK (Term.bound i "") :: cs
+        | rands (Bound i,  cs)   = AtomK (Term.bound i) :: cs
   in case (head_of t) of
       Var _ => VarK :: cs
     | Abs _ => VarK :: cs
     | _     => rands(t,cs)
   end;

         | rands t (Net{comb,atoms,...}, nets) =
             case t of
                 f$t => foldr (matching unif t) nets (rands f (comb,[]))
               | Const(c,_) => look1 (atoms, c) nets
               | Free(c,_)  => look1 (atoms, c) nets
-              | Bound i    => look1 (atoms, Term.bound i "") nets
+              | Bound i    => look1 (atoms, Term.bound i) nets
               | _          => nets
   in
      case net of
          Leaf _ => nets
        | Net{var,...} =>