src/Pure/Isar/proof_context.ML
changeset 15966 73cf5ef8ed20
parent 15964 f2074e12d1d4
child 15974 cef3d89d49d4
     1.1 --- a/src/Pure/Isar/proof_context.ML	Mon May 16 10:29:15 2005 +0200
     1.2 +++ b/src/Pure/Isar/proof_context.ML	Tue May 17 01:24:19 2005 +0200
     1.3 @@ -1538,14 +1538,6 @@
     1.4  
     1.5  (* ------------</filter constructions> *)
     1.6  
     1.7 -(* collect all the Var statements in a term *)
     1.8 -fun vars_of_term (Const _) = []
     1.9 -  | vars_of_term (Free _) = []
    1.10 -  | vars_of_term (Bound _) = []
    1.11 -  | vars_of_term (Abs (_,_,t)) = vars_of_term t
    1.12 -  | vars_of_term (v as (Var _)) = [v]
    1.13 -  | vars_of_term (x $ y) = vars_of_term x @ (vars_of_term y);
    1.14 -
    1.15  (* elimination rule: conclusion is a Var and 
    1.16     no Var in the conclusion appears in the major premise
    1.17     Note: only makes sense if the major premise already matched the assumption 
    1.18 @@ -1555,10 +1547,10 @@
    1.19      val {prop, ...} = rep_thm thm;
    1.20      val concl = rem_top_c (Logic.strip_imp_concl prop);
    1.21      val major_prem = hd (Logic.strip_imp_prems prop);
    1.22 -    val prem_vars = distinct (vars_of_term major_prem);
    1.23 -    val concl_vars = distinct (vars_of_term concl);
    1.24 +    val prem_vars = distinct (Drule.vars_of_terms [major_prem]);
    1.25 +    val concl_vars = distinct (Drule.vars_of_terms [concl]);
    1.26    in
    1.27 -    Term.is_Var concl andalso ((prem_vars inter concl_vars) = [])
    1.28 +    Term.is_Var concl andalso (prem_vars inter concl_vars) = []
    1.29    end;
    1.30  
    1.31  fun crit2str (Name name) = "name:" ^ name