1.1 --- a/src/HOL/Tools/meson.ML	Wed May 19 11:30:56 2004 +0200
     1.2 +++ b/src/HOL/Tools/meson.ML	Wed May 19 11:31:26 2004 +0200
     1.3 @@ -51,6 +51,8 @@
     1.4   (*Are any of the constants in "bs" present in the term?*)
     1.5   fun has_consts bs =
     1.6     let fun has (Const(a,_)) = a mem bs
     1.7 +	 | has (Const ("Hilbert_Choice.Eps",_) $ _) = false
     1.8 +                      (*ignore constants within @-terms*)
     1.9           | has (f$u) = has f orelse has u
    1.10           | has (Abs(_,_,t)) = has t
    1.11           | has _ = false
    1.12 @@ -94,8 +96,10 @@
    1.13   (*Conjunctive normal form, detecting tautologies early.
    1.14     Strips universal quantifiers and breaks up conjunctions. *)
    1.15   fun cnf_aux seen (th,ths) =
    1.16 -   if taut_lits (literals(prop_of th) @ seen)  then ths
    1.17 -   else if not (has_consts ["All","op &"] (prop_of th))  then th::ths
    1.18 +   if taut_lits (literals(prop_of th) @ seen)  
    1.19 +   then ths     (*tautology ignored*)
    1.20 +   else if not (has_consts ["All","op &"] (prop_of th))  
    1.21 +   then th::ths (*no work to do, terminate*)
    1.22     else (*conjunction?*)
    1.23           cnf_aux seen (th RS conjunct1,
    1.24                         cnf_aux seen (th RS conjunct2, ths))