Term.bound;

--- a/src/Pure/meta_simplifier.ML	Thu Jul 28 15:19:54 2005 +0200
+++ b/src/Pure/meta_simplifier.ML	Thu Jul 28 15:19:55 2005 +0200
@@ -916,7 +916,7 @@
        (case term_of t0 of
            Abs (a, T, t) =>
              let
-                 val (v, t') = Thm.dest_abs (SOME ("." ^ a ^ "." ^ string_of_int bounds)) t0;
+                 val (v, t') = Thm.dest_abs (SOME (Term.bound bounds a)) t0;
                  val ss' = incr_bounds ss;
                  val skel' = case skel of Abs (_, _, sk) => sk | _ => skel0;
              in case botc skel' ss' t' of

--- a/src/Pure/net.ML	Thu Jul 28 15:19:54 2005 +0200
+++ b/src/Pure/net.ML	Thu Jul 28 15:19:55 2005 +0200
@@ -39,9 +39,6 @@
 
 datatype key = CombK | VarK | AtomK of string;
 
-(*Bound variables*)
-fun string_of_bound i = "*B*" ^ chr (i div 256) ^ chr (i mod 256);
-
 (*Keys are preorder lists of symbols -- Combinations, Vars, Atoms.
   Any term whose head is a Var is regarded entirely as a Var.
   Abstractions are also regarded as Vars;  this covers eta-conversion
@@ -51,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 (string_of_bound i) :: cs
+        | rands (Bound i,  cs)   = AtomK (Term.bound i "") :: cs
   in case (head_of t) of
       Var _ => VarK :: cs
     | Abs _ => VarK :: cs
@@ -184,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, string_of_bound i) nets
+              | Bound i    => look1 (atoms, Term.bound i "") nets
               | _          => nets
   in
      case net of