# HG changeset patch
# User kleing
# Date 1116285859 -7200
# Node ID 73cf5ef8ed20575b303debb26f6e56eaa4ec706e
# Parent  f422f82834914a7208c0cb2f11662c1252e95fe9
use Drule.vars_of_terms

diff -r f422f8283491 -r 73cf5ef8ed20 src/Pure/Isar/proof_context.ML
--- a/src/Pure/Isar/proof_context.ML	Mon May 16 10:29:15 2005 +0200
+++ b/src/Pure/Isar/proof_context.ML	Tue May 17 01:24:19 2005 +0200
@@ -1538,14 +1538,6 @@
 
 (* ------------</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 
@@ -1555,10 +1547,10 @@
     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);
+    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) = [])
+    Term.is_Var concl andalso (prem_vars inter concl_vars) = []
   end;
 
 fun crit2str (Name name) = "name:" ^ name