Term.declare_term_names;
authorwenzelm
Tue Jul 18 20:01:41 2006 +0200 (2006-07-18)
changeset 20146d8cf6eb9baf9
parent 20145 922b4e7b8efd
child 20147 7aa076a45cb4
Term.declare_term_names;
src/Pure/Syntax/syn_trans.ML
src/Pure/meta_simplifier.ML
     1.1 --- a/src/Pure/Syntax/syn_trans.ML	Tue Jul 18 17:10:22 2006 +0200
     1.2 +++ b/src/Pure/Syntax/syn_trans.ML	Tue Jul 18 20:01:41 2006 +0200
     1.3 @@ -383,9 +383,9 @@
     1.4  
     1.5  (* dependent / nondependent quantifiers *)
     1.6  
     1.7 -fun variant_abs' (x, T, B) =
     1.8 -  let val x' = Name.variant (add_term_names (B, [])) x in
     1.9 -    (x', subst_bound (mark_boundT (x', T), B))
    1.10 +fun variant_abs' (x, T, b) =
    1.11 +  let val ([x'], _) = Name.variants [x] (Term.declare_term_names b Name.context) in
    1.12 +    (x', subst_bound (mark_boundT (x', T), b))
    1.13    end;
    1.14  
    1.15  fun dependent_tr' (q, r) (A :: Abs (x, T, B) :: ts) =
     2.1 --- a/src/Pure/meta_simplifier.ML	Tue Jul 18 17:10:22 2006 +0200
     2.2 +++ b/src/Pure/meta_simplifier.ML	Tue Jul 18 20:01:41 2006 +0200
     2.3 @@ -257,8 +257,8 @@
     2.4  
     2.5  fun show_bounds (Simpset ({bounds = (_, bs), ...}, _)) t =
     2.6    let
     2.7 -    val used = Term.add_term_names (t, []);
     2.8 -    val xs = rev (Name.variant_list used (rev (map #2 bs)));
     2.9 +    val names = Term.declare_term_names t Name.context;
    2.10 +    val xs = rev (#1 (Name.variants (rev (map #2 bs)) names));
    2.11      fun subst (((b, T), _), x') = (Free (b, T), Syntax.mark_boundT (x', T));
    2.12    in Term.subst_atomic (ListPair.map subst (bs, xs)) t end;
    2.13