# HG changeset patch
# User paulson
# Date 1084959086 -7200
# Node ID c1fd297712ba93511b693c252b26eb8141e7a58e
# Parent  bd349ff7907aa5a5c28acb4ea7b6fecba7126f8a
has_consts now handles the @-operator

diff -r bd349ff7907a -r c1fd297712ba src/HOL/Tools/meson.ML
--- a/src/HOL/Tools/meson.ML	Wed May 19 11:30:56 2004 +0200
+++ b/src/HOL/Tools/meson.ML	Wed May 19 11:31:26 2004 +0200
@@ -51,6 +51,8 @@
  (*Are any of the constants in "bs" present in the term?*)
  fun has_consts bs =
    let fun has (Const(a,_)) = a mem bs
+	 | has (Const ("Hilbert_Choice.Eps",_) $ _) = false
+                      (*ignore constants within @-terms*)
          | has (f$u) = has f orelse has u
          | has (Abs(_,_,t)) = has t
          | has _ = false
@@ -94,8 +96,10 @@
  (*Conjunctive normal form, detecting tautologies early.
    Strips universal quantifiers and breaks up conjunctions. *)
  fun cnf_aux seen (th,ths) =
-   if taut_lits (literals(prop_of th) @ seen)  then ths
-   else if not (has_consts ["All","op &"] (prop_of th))  then th::ths
+   if taut_lits (literals(prop_of th) @ seen)  
+   then ths     (*tautology ignored*)
+   else if not (has_consts ["All","op &"] (prop_of th))  
+   then th::ths (*no work to do, terminate*)
    else (*conjunction?*)
          cnf_aux seen (th RS conjunct1,
                        cnf_aux seen (th RS conjunct2, ths))