# HG changeset patch # User berghofe # Date 1037198115 -3600 # Node ID 34ef15959ce731dee6a16f2d5dcda3f991a03532 # Parent 82d7fc25a2250df516a040f9ca5a85cde95e7ac5 Fixed name clash problem in forall_elim_var. diff -r 82d7fc25a225 -r 34ef15959ce7 src/Pure/pure_thy.ML --- a/src/Pure/pure_thy.ML Wed Nov 13 15:34:35 2002 +0100 +++ b/src/Pure/pure_thy.ML Wed Nov 13 15:35:15 2002 +0100 @@ -378,14 +378,15 @@ (* forall_elim_vars (belongs to drule.ML) *) -(*Replace outermost quantified variable by Var of given index. - Could clash with Vars already present.*) +(*Replace outermost quantified variable by Var of given index.*) fun forall_elim_var i th = let val {prop,sign,...} = rep_thm th in case prop of - Const("all",_) $ Abs(a,T,_) => - forall_elim (cterm_of sign (Var((a,i), T))) th - | _ => raise THM("forall_elim_var", i, [th]) + Const ("all", _) $ Abs (a, T, _) => + let val used = map (fst o fst) + (filter (equal i o snd o fst) (Term.add_vars ([], prop))) + in forall_elim (cterm_of sign (Var ((variant used a, i), T))) th end + | _ => raise THM ("forall_elim_var", i, [th]) end; (*Repeat forall_elim_var until all outer quantifiers are removed*)