Mercurial Mercurial > repos > isabelle / changeset
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | raw | gz | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
Name.bound;
authorwenzelm
Tue, 11 Jul 2006 12:17:05 +0200
changeset 20080 1398063aa271
parent 20079 ec5c8584487c
child 20081 c9da24b69fda
Name.bound;
src/Pure/net.ML file | annotate | diff | comparison | revisions 
--- 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
isabelle