# HG changeset patch
# User wenzelm
# Date 1152613025 -7200
# Node ID 1398063aa271ea317e19c2395a4f37cb9797d696
# Parent  ec5c8584487cf2394c2d2fe9697ec025f79f86a2
Name.bound;

diff -r ec5c8584487c -r 1398063aa271 src/Pure/net.ML
--- a/src/Pure/net.ML	Tue Jul 11 12:17:04 2006 +0200
+++ b/src/Pure/net.ML	Tue Jul 11 12:17:05 2006 +0200
@@ -49,7 +49,7 @@
   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 (Name.bound i) :: cs
   in case (head_of t) of
       Var _ => VarK :: cs
     | Abs _ => VarK :: cs
@@ -182,7 +182,7 @@
                 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, Name.bound i) nets
               | _          => nets
   in
      case net of