replaced Term.variant(list) by Name.variant(_list);
authorwenzelm
Tue Jul 11 12:17:04 2006 +0200 (2006-07-11)
changeset 20079ec5c8584487c
parent 20078 f4122d7494f3
child 20080 1398063aa271
replaced Term.variant(list) by Name.variant(_list);
Name.bound;
src/Pure/meta_simplifier.ML
src/Pure/pattern.ML
     1.1 --- a/src/Pure/meta_simplifier.ML	Tue Jul 11 12:17:03 2006 +0200
     1.2 +++ b/src/Pure/meta_simplifier.ML	Tue Jul 11 12:17:04 2006 +0200
     1.3 @@ -258,7 +258,7 @@
     1.4  fun show_bounds (Simpset ({bounds = (_, bs), ...}, _)) t =
     1.5    let
     1.6      val used = Term.add_term_names (t, []);
     1.7 -    val xs = rev (Term.variantlist (rev (map #2 bs), used));
     1.8 +    val xs = rev (Name.variant_list used (rev (map #2 bs)));
     1.9      fun subst (((b, T), _), x') = (Free (b, T), Syntax.mark_boundT (x', T));
    1.10    in Term.subst_atomic (ListPair.map subst (bs, xs)) t end;
    1.11  
    1.12 @@ -964,7 +964,7 @@
    1.13         (case term_of t0 of
    1.14             Abs (a, T, t) =>
    1.15               let
    1.16 -                 val b = Term.bound (#1 bounds);
    1.17 +                 val b = Name.bound (#1 bounds);
    1.18                   val (v, t') = Thm.dest_abs (SOME b) t0;
    1.19                   val b' = #1 (Term.dest_Free (Thm.term_of v));
    1.20                   val _ = conditional (b <> b') (fn () =>
    1.21 @@ -1148,7 +1148,7 @@
    1.22    let
    1.23      val Simpset ({bounds = (_, bounds), ...}, _) = ss;
    1.24      val bs = fold_aterms (fn Free (x, _) =>
    1.25 -        if Term.is_bound x andalso not (AList.defined eq_bound bounds x)
    1.26 +        if Name.is_bound x andalso not (AList.defined eq_bound bounds x)
    1.27          then insert (op =) x else I
    1.28        | _ => I) (term_of ct) [];
    1.29    in
     2.1 --- a/src/Pure/pattern.ML	Tue Jul 11 12:17:03 2006 +0200
     2.2 +++ b/src/Pure/pattern.ML	Tue Jul 11 12:17:04 2006 +0200
     2.3 @@ -413,7 +413,7 @@
     2.4  fun matches_subterm thy (pat,obj) =
     2.5    let fun msub(bounds,obj) = matches thy (pat,obj) orelse
     2.6              (case obj of
     2.7 -              Abs(x,T,t) => let val y = variant bounds x
     2.8 +              Abs(x,T,t) => let val y = Name.variant bounds x
     2.9                                  val f = Free(":" ^ y,T)
    2.10                              in msub(x::bounds,subst_bound(f,t)) end
    2.11              | s$t => msub(bounds,s) orelse msub(bounds,t)
    2.12 @@ -442,7 +442,7 @@
    2.13  
    2.14      fun variant_absfree bounds (x, T, t) =
    2.15        let
    2.16 -        val (x', t') = Term.dest_abs (Term.bound bounds, T, t);
    2.17 +        val (x', t') = Term.dest_abs (Name.bound bounds, T, t);
    2.18          fun abs u = Abs (x, T, abstract_over (Free (x', T), u));
    2.19        in (abs, t') end;
    2.20