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)