1.1 --- a/src/HOL/Tools/meson.ML	Wed Jul 05 16:24:10 2006 +0200
     1.2 +++ b/src/HOL/Tools/meson.ML	Wed Jul 05 16:24:28 2006 +0200
     1.3 @@ -279,7 +279,7 @@
     1.4    incomplete, since when actually called, the only connectives likely to
     1.5    remain are & | Not.*)  
     1.6  val is_conn = member (op =)
     1.7 -    ["Trueprop", "HOL.tag", "op &", "op |", "op -->", "op =", "Not", 
     1.8 +    ["Trueprop", "op &", "op |", "op -->", "op =", "Not", 
     1.9       "All", "Ex", "Ball", "Bex"];
    1.10  
    1.11  (*True if the term contains a function where the type of any argument contains
    1.12 @@ -386,13 +386,11 @@
    1.13             (tryres(th, [conj_forward,disj_forward,all_forward,ex_forward]))
    1.14      handle THM _ => th;
    1.15  
    1.16 -(*The simplification removes defined quantifiers and occurrences of True and False, 
    1.17 -  as well as tags applied to True and False. nnf_ss also includes the one-point simprocs,
    1.18 +(*The simplification removes defined quantifiers and occurrences of True and False. 
    1.19 +  nnf_ss also includes the one-point simprocs,
    1.20    which are needed to avoid the various one-point theorems from generating junk clauses.*)
    1.21 -val tag_True = thm "tag_True";
    1.22 -val tag_False = thm "tag_False";
    1.23  val nnf_simps =
    1.24 -     [simp_implies_def, Ex1_def, Ball_def, Bex_def, tag_True, tag_False, if_True, 
    1.25 +     [simp_implies_def, Ex1_def, Ball_def, Bex_def, if_True, 
    1.26        if_False, if_cancel, if_eq_cancel, cases_simp];
    1.27  val nnf_extra_simps =
    1.28        thms"split_ifs" @ ex_simps @ all_simps @ simp_thms;