src/Pure/Isar/proof_context.ML

     prem_matches_name_thm prems      
   end;
 
 (* ------------</filter constructions> *)
 
-(* collect all the Var statements in a term *)
-fun vars_of_term (Const _) = []
-  | vars_of_term (Free _) = []
-  | vars_of_term (Bound _) = []
-  | vars_of_term (Abs (_,_,t)) = vars_of_term t
-  | vars_of_term (v as (Var _)) = [v]
-  | vars_of_term (x $ y) = vars_of_term x @ (vars_of_term y);
-
 (* elimination rule: conclusion is a Var and 
    no Var in the conclusion appears in the major premise
    Note: only makes sense if the major premise already matched the assumption 
          of some goal! *)
 fun is_elim_rule thm =
   let
     val {prop, ...} = rep_thm thm;
     val concl = rem_top_c (Logic.strip_imp_concl prop);
     val major_prem = hd (Logic.strip_imp_prems prop);
-    val prem_vars = distinct (vars_of_term major_prem);
-    val concl_vars = distinct (vars_of_term concl);
-  in
-    Term.is_Var concl andalso ((prem_vars inter concl_vars) = [])
+    val prem_vars = distinct (Drule.vars_of_terms [major_prem]);
+    val concl_vars = distinct (Drule.vars_of_terms [concl]);
+  in
+    Term.is_Var concl andalso (prem_vars inter concl_vars) = []
   end;
 
 fun crit2str (Name name) = "name:" ^ name
   | crit2str Elim = "elim"
   | crit2str Intro = "intro"