# HG changeset patch
# User wenzelm
# Date 1185712196 -7200
# Node ID 0d5cf52ebf87ddb43d6cc964e8e5ede4fe4d003e
# Parent  273698405054f16182a1692051e50695d299f9e2
proper simproc_setup for "neq", "let_simp";
removed dead code;

diff -r 273698405054 -r 0d5cf52ebf87 src/HOL/Tools/meson.ML
--- a/src/HOL/Tools/meson.ML	Sun Jul 29 14:29:54 2007 +0200
+++ b/src/HOL/Tools/meson.ML	Sun Jul 29 14:29:56 2007 +0200
@@ -61,7 +61,6 @@
 val disj_FalseD1 = thm "meson_disj_FalseD1";
 val disj_FalseD2 = thm "meson_disj_FalseD2";
 
-val depth_limit = ref 2000;
 
 (**** Operators for forward proof ****)
 
@@ -505,8 +504,8 @@
       thms"split_ifs" @ ex_simps @ all_simps @ simp_thms;
 
 val nnf_ss =
-    HOL_basic_ss addsimps nnf_extra_simps 
-                 addsimprocs [defALL_regroup,defEX_regroup,neq_simproc,let_simproc];
+  HOL_basic_ss addsimps nnf_extra_simps 
+    addsimprocs [defALL_regroup,defEX_regroup, @{simproc neq}, @{simproc let_simp}];
 
 fun make_nnf th = case prems_of th of
     [] => th |> rewrite_rule (map safe_mk_meta_eq nnf_simps)