canonical Term.add_var_names;
authorwenzelm
Tue Dec 30 21:46:48 2008 +0100 (2008-12-30)
changeset 29258bce03c644efb
parent 29257 660234d959f7
child 29259 4621affa5c79
canonical Term.add_var_names;
src/HOL/Bali/AxExample.thy
src/HOL/Library/Efficient_Nat.thy
     1.1 --- a/src/HOL/Bali/AxExample.thy	Tue Dec 30 21:46:14 2008 +0100
     1.2 +++ b/src/HOL/Bali/AxExample.thy	Tue Dec 30 21:46:48 2008 +0100
     1.3 @@ -41,7 +41,7 @@
     1.4  
     1.5  ML {*
     1.6  fun inst1_tac ctxt s t st =
     1.7 -  case AList.lookup (op =) (rev (Term.add_varnames (Thm.prop_of st) [])) s of
     1.8 +  case AList.lookup (op =) (rev (Term.add_var_names (Thm.prop_of st) [])) s of
     1.9    SOME i => instantiate_tac ctxt [((s, i), t)] st | NONE => Seq.empty;
    1.10  
    1.11  val ax_tac =
     2.1 --- a/src/HOL/Library/Efficient_Nat.thy	Tue Dec 30 21:46:14 2008 +0100
     2.2 +++ b/src/HOL/Library/Efficient_Nat.thy	Tue Dec 30 21:46:48 2008 +0100
     2.3 @@ -127,7 +127,7 @@
     2.4  fun remove_suc thy thms =
     2.5    let
     2.6      val vname = Name.variant (map fst
     2.7 -      (fold (Term.add_varnames o Thm.full_prop_of) thms [])) "x";
     2.8 +      (fold (Term.add_var_names o Thm.full_prop_of) thms [])) "x";
     2.9      val cv = cterm_of thy (Var ((vname, 0), HOLogic.natT));
    2.10      fun lhs_of th = snd (Thm.dest_comb
    2.11        (fst (Thm.dest_comb (snd (Thm.dest_comb (cprop_of th))))));
    2.12 @@ -180,7 +180,7 @@
    2.13  fun remove_suc_clause thy thms =
    2.14    let
    2.15      val vname = Name.variant (map fst
    2.16 -      (fold (Term.add_varnames o Thm.full_prop_of) thms [])) "x";
    2.17 +      (fold (Term.add_var_names o Thm.full_prop_of) thms [])) "x";
    2.18      fun find_var (t as Const (@{const_name Suc}, _) $ (v as Var _)) = SOME (t, v)
    2.19        | find_var (t $ u) = (case find_var t of NONE => find_var u | x => x)
    2.20        | find_var _ = NONE;