nameless Term.bound;
authorwenzelm
Mon Aug 01 19:20:40 2005 +0200 (2005-08-01)
changeset 1698668bc6dbea7d6
parent 16985 7df8abe926c3
child 16987 9ed901d738ba
nameless Term.bound;
src/Pure/net.ML
src/Pure/pattern.ML
     1.1 --- a/src/Pure/net.ML	Mon Aug 01 19:20:39 2005 +0200
     1.2 +++ b/src/Pure/net.ML	Mon Aug 01 19:20:40 2005 +0200
     1.3 @@ -48,7 +48,7 @@
     1.4    let fun rands (f$t, cs) = CombK :: rands (f, add_key_of_terms(t, cs))
     1.5          | rands (Const(c,_), cs) = AtomK c :: cs
     1.6          | rands (Free(c,_),  cs) = AtomK c :: cs
     1.7 -        | rands (Bound i,  cs)   = AtomK (Term.bound i "") :: cs
     1.8 +        | rands (Bound i,  cs)   = AtomK (Term.bound i) :: cs
     1.9    in case (head_of t) of
    1.10        Var _ => VarK :: cs
    1.11      | Abs _ => VarK :: cs
    1.12 @@ -181,7 +181,7 @@
    1.13                  f$t => foldr (matching unif t) nets (rands f (comb,[]))
    1.14                | Const(c,_) => look1 (atoms, c) nets
    1.15                | Free(c,_)  => look1 (atoms, c) nets
    1.16 -              | Bound i    => look1 (atoms, Term.bound i "") nets
    1.17 +              | Bound i    => look1 (atoms, Term.bound i) nets
    1.18                | _          => nets
    1.19    in
    1.20       case net of
     2.1 --- a/src/Pure/pattern.ML	Mon Aug 01 19:20:39 2005 +0200
     2.2 +++ b/src/Pure/pattern.ML	Mon Aug 01 19:20:40 2005 +0200
     2.3 @@ -477,7 +477,7 @@
     2.4  
     2.5      fun variant_absfree bounds (x, T, t) =
     2.6        let
     2.7 -        val (x', t') = Term.dest_abs (Term.bound bounds x, T, t);
     2.8 +        val (x', t') = Term.dest_abs (Term.bound bounds, T, t);
     2.9          fun abs u = Abs (x, T, abstract_over (Free (x', T), u));
    2.10        in (abs, t') end;
    2.11