1.1 --- a/src/HOL/Tools/meson.ML	Sun Jul 29 14:29:54 2007 +0200
     1.2 +++ b/src/HOL/Tools/meson.ML	Sun Jul 29 14:29:56 2007 +0200
     1.3 @@ -61,7 +61,6 @@
     1.4  val disj_FalseD1 = thm "meson_disj_FalseD1";
     1.5  val disj_FalseD2 = thm "meson_disj_FalseD2";
     1.6  
     1.7 -val depth_limit = ref 2000;
     1.8  
     1.9  (**** Operators for forward proof ****)
    1.10  
    1.11 @@ -505,8 +504,8 @@
    1.12        thms"split_ifs" @ ex_simps @ all_simps @ simp_thms;
    1.13  
    1.14  val nnf_ss =
    1.15 -    HOL_basic_ss addsimps nnf_extra_simps 
    1.16 -                 addsimprocs [defALL_regroup,defEX_regroup,neq_simproc,let_simproc];
    1.17 +  HOL_basic_ss addsimps nnf_extra_simps 
    1.18 +    addsimprocs [defALL_regroup,defEX_regroup, @{simproc neq}, @{simproc let_simp}];
    1.19  
    1.20  fun make_nnf th = case prems_of th of
    1.21      [] => th |> rewrite_rule (map safe_mk_meta_eq nnf_simps)