src/HOL/Tools/res_clause.ML
changeset 21470 7c1b59ddcd56
parent 21432 625797c592b2
child 21509 6c5755ad9cae
     1.1 --- a/src/HOL/Tools/res_clause.ML	Wed Nov 22 19:55:22 2006 +0100
     1.2 +++ b/src/HOL/Tools/res_clause.ML	Wed Nov 22 20:08:07 2006 +0100
     1.3 @@ -417,35 +417,14 @@
     1.4  	  (vss, fs union fss)
     1.5        end;
     1.6  
     1.7 -(** Too general means, positive equality literal with a variable X as one operand,
     1.8 -  when X does not occur properly in the other operand. This rules out clearly
     1.9 -  inconsistent clauses such as V=a|V=b, though it by no means guarantees soundness. **)
    1.10 -
    1.11 -fun occurs a (UVar(b,_)) = a=b
    1.12 -  | occurs a (Fun (_,_,ts)) = exists (occurs a) ts
    1.13 -
    1.14 -(*Is the first operand a variable that does not properly occur in the second operand?*)
    1.15 -fun too_general_terms (UVar _, UVar _) = false
    1.16 -  | too_general_terms (Fun _, _) = false
    1.17 -  | too_general_terms (UVar (a,_), t) = not (occurs a t);
    1.18 -
    1.19 -fun too_general_lit (Literal (true, Predicate("equal",_,[x,y]))) =
    1.20 -      too_general_terms (x,y) orelse too_general_terms(y,x)
    1.21 -  | too_general_lit _ = false;
    1.22 -
    1.23 -
    1.24  
    1.25  (** make axiom and conjecture clauses. **)
    1.26  
    1.27  exception MAKE_CLAUSE;
    1.28  fun make_clause (clause_id, axiom_name, th, kind) =
    1.29 -  let val term = prop_of th
    1.30 -      val (lits,types_sorts) = literals_of_term term
    1.31 +  let val (lits,types_sorts) = literals_of_term (prop_of th)
    1.32    in if forall isFalse lits 
    1.33       then error "Problem too trivial for resolution (empty clause)"
    1.34 -     else if kind=Axiom andalso forall too_general_lit lits 
    1.35 -     then (Output.debug ("Omitting " ^ axiom_name ^ ": equalities are too general"); 
    1.36 -           raise MAKE_CLAUSE)
    1.37       else Clause {clause_id = clause_id, axiom_name = axiom_name, th = th, 
    1.38                    kind = kind, literals = lits, types_sorts = types_sorts}
    1.39    end;