renamed add_term_varnames to Term.add_varnames (cf. Term.add_vars etc.);
authorwenzelm
Tue Jul 25 21:18:02 2006 +0200 (2006-07-25)
changeset 201969a19e4de6e2e
parent 20195 ae79b9ad7224
child 20197 ffc64d90fc1f
renamed add_term_varnames to Term.add_varnames (cf. Term.add_vars etc.);
src/HOL/Library/EfficientNat.thy
src/Pure/Isar/locale.ML
     1.1 --- a/src/HOL/Library/EfficientNat.thy	Tue Jul 25 21:18:01 2006 +0200
     1.2 +++ b/src/HOL/Library/EfficientNat.thy	Tue Jul 25 21:18:02 2006 +0200
     1.3 @@ -154,7 +154,7 @@
     1.4    let
     1.5      val Suc_if_eq' = Thm.transfer thy Suc_if_eq;
     1.6      val vname = Name.variant (map fst
     1.7 -      (fold (add_term_varnames o Thm.full_prop_of) thms [])) "x";
     1.8 +      (fold (Term.add_varnames o Thm.full_prop_of) thms [])) "x";
     1.9      val cv = cterm_of Main.thy (Var ((vname, 0), HOLogic.natT));
    1.10      fun lhs_of th = snd (Thm.dest_comb
    1.11        (fst (Thm.dest_comb (snd (Thm.dest_comb (cprop_of th))))));
    1.12 @@ -207,7 +207,7 @@
    1.13    let
    1.14      val Suc_clause' = Thm.transfer thy Suc_clause;
    1.15      val vname = Name.variant (map fst
    1.16 -      (fold (add_term_varnames o Thm.full_prop_of) thms [])) "x";
    1.17 +      (fold (Term.add_varnames o Thm.full_prop_of) thms [])) "x";
    1.18      fun find_var (t as Const ("Suc", _) $ (v as Var _)) = SOME (t, v)
    1.19        | find_var (t $ u) = (case find_var t of NONE => find_var u | x => x)
    1.20        | find_var _ = NONE;
     2.1 --- a/src/Pure/Isar/locale.ML	Tue Jul 25 21:18:01 2006 +0200
     2.2 +++ b/src/Pure/Isar/locale.ML	Tue Jul 25 21:18:02 2006 +0200
     2.3 @@ -2090,7 +2090,7 @@
     2.4      fun sorts (a, i) = AList.lookup (op =) tvars (a, i);
     2.5      val (vs, vinst) = read_terms thy_ctxt sorts used given_insts;
     2.6      val vars = foldl Term.add_term_tvar_ixns [] vs \\ map fst tvars;
     2.7 -    val vars' = fold Term.add_term_varnames vs vars;
     2.8 +    val vars' = fold Term.add_varnames vs vars;
     2.9      val _ = if null vars' then ()
    2.10           else error ("Illegal schematic variable(s) in instantiation: " ^
    2.11             commas_quote (map Syntax.string_of_vname vars'));