src/Provers/classical.ML
changeset 29267 8615b4f54047
parent 26938 64e850c3da9e
child 30190 479806475f3c
     1.1 --- a/src/Provers/classical.ML	Wed Dec 31 00:08:13 2008 +0100
     1.2 +++ b/src/Provers/classical.ML	Wed Dec 31 00:08:13 2008 +0100
     1.3 @@ -1,7 +1,5 @@
     1.4  (*  Title:      Provers/classical.ML
     1.5 -    ID:         $Id$
     1.6      Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
     1.7 -    Copyright   1992  University of Cambridge
     1.8  
     1.9  Theorem prover for classical reasoning, including predicate calculus, set
    1.10  theory, etc.
    1.11 @@ -810,9 +808,7 @@
    1.12      (fn (prem,i) =>
    1.13        let val deti =
    1.14            (*No Vars in the goal?  No need to backtrack between goals.*)
    1.15 -          case term_vars prem of
    1.16 -              []        => DETERM
    1.17 -            | _::_      => I
    1.18 +          if exists_subterm (fn Var _ => true | _ => false) prem then DETERM else I
    1.19        in  SELECT_GOAL (TRY (safe_tac cs) THEN
    1.20                         DEPTH_SOLVE (deti (depth_tac cs m 1))) i
    1.21        end);