src/Pure/pattern.ML
changeset 20079 ec5c8584487c
parent 19880 1b0d48257caf
child 20098 19871ee094b1
     1.1 --- a/src/Pure/pattern.ML	Tue Jul 11 12:17:03 2006 +0200
     1.2 +++ b/src/Pure/pattern.ML	Tue Jul 11 12:17:04 2006 +0200
     1.3 @@ -413,7 +413,7 @@
     1.4  fun matches_subterm thy (pat,obj) =
     1.5    let fun msub(bounds,obj) = matches thy (pat,obj) orelse
     1.6              (case obj of
     1.7 -              Abs(x,T,t) => let val y = variant bounds x
     1.8 +              Abs(x,T,t) => let val y = Name.variant bounds x
     1.9                                  val f = Free(":" ^ y,T)
    1.10                              in msub(x::bounds,subst_bound(f,t)) end
    1.11              | s$t => msub(bounds,s) orelse msub(bounds,t)
    1.12 @@ -442,7 +442,7 @@
    1.13  
    1.14      fun variant_absfree bounds (x, T, t) =
    1.15        let
    1.16 -        val (x', t') = Term.dest_abs (Term.bound bounds, T, t);
    1.17 +        val (x', t') = Term.dest_abs (Name.bound bounds, T, t);
    1.18          fun abs u = Abs (x, T, abstract_over (Free (x', T), u));
    1.19        in (abs, t') end;
    1.20