1.1 --- a/src/Pure/drule.ML	Thu Oct 21 18:04:07 1999 +0200
     1.2 +++ b/src/Pure/drule.ML	Thu Oct 21 18:41:51 1999 +0200
     1.3 @@ -227,20 +227,8 @@
     1.4           th
     1.5      end;
     1.6  
     1.7 -(*Replace outermost quantified variable by Var of given index.
     1.8 -    Could clash with Vars already present.*)
     1.9 -fun forall_elim_var i th =
    1.10 -    let val {prop,sign,...} = rep_thm th
    1.11 -    in case prop of
    1.12 -          Const("all",_) $ Abs(a,T,_) =>
    1.13 -              forall_elim (cterm_of sign (Var((a,i), T)))  th
    1.14 -        | _ => raise THM("forall_elim_var", i, [th])
    1.15 -    end;
    1.16 -
    1.17 -(*Repeat forall_elim_var until all outer quantifiers are removed*)
    1.18 -fun forall_elim_vars i th =
    1.19 -    forall_elim_vars i (forall_elim_var i th)
    1.20 -        handle THM _ => th;
    1.21 +val forall_elim_var = PureThy.forall_elim_var;
    1.22 +val forall_elim_vars = PureThy.forall_elim_vars;
    1.23  
    1.24  (*Specialization over a list of cterms*)
    1.25  fun forall_elim_list cts th = foldr (uncurry forall_elim) (rev cts, th);