# HG changeset patch # User wenzelm # Date 1122556795 -7200 # Node ID 04bdd18e0ad1f9bc6a139386530fa0844f6cf06c # Parent 0822bbdd6769f5d4d64967e5a8a0c681636d06ce Term.bound; diff -r 0822bbdd6769 -r 04bdd18e0ad1 src/Pure/meta_simplifier.ML --- 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 diff -r 0822bbdd6769 -r 04bdd18e0ad1 src/Pure/net.ML --- 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