# HG changeset patch
# User wenzelm
# Date 1122916840 -7200
# Node ID 68bc6dbea7d6a4b7e4bffafcc55843d5cacc4b74
# Parent  7df8abe926c35757277f006c3804306593326009
nameless Term.bound;

diff -r 7df8abe926c3 -r 68bc6dbea7d6 src/Pure/net.ML
--- a/src/Pure/net.ML	Mon Aug 01 19:20:39 2005 +0200
+++ b/src/Pure/net.ML	Mon Aug 01 19:20:40 2005 +0200
@@ -48,7 +48,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 (Term.bound i) :: cs
   in case (head_of t) of
       Var _ => VarK :: cs
     | Abs _ => VarK :: cs
@@ -181,7 +181,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, Term.bound i) nets
               | _          => nets
   in
      case net of
diff -r 7df8abe926c3 -r 68bc6dbea7d6 src/Pure/pattern.ML
--- a/src/Pure/pattern.ML	Mon Aug 01 19:20:39 2005 +0200
+++ b/src/Pure/pattern.ML	Mon Aug 01 19:20:40 2005 +0200
@@ -477,7 +477,7 @@
 
     fun variant_absfree bounds (x, T, t) =
       let
-        val (x', t') = Term.dest_abs (Term.bound bounds x, T, t);
+        val (x', t') = Term.dest_abs (Term.bound bounds, T, t);
         fun abs u = Abs (x, T, abstract_over (Free (x', T), u));
       in (abs, t') end;