# HG changeset patch
# User krauss
# Date 1273411724 -7200
# Node ID acb789f3936bf1849abb9f0ba6a1d80e2a6a5d88
# Parent  ef97c50068402553a9bc714fab6987826cf45699
do not redeclare [simp] rules, to avoid "duplicate rewrite rule" warnings

diff -r ef97c5006840 -r acb789f3936b src/HOL/Tools/Function/mutual.ML
--- a/src/HOL/Tools/Function/mutual.ML	Sun May 09 12:00:43 2010 +0200
+++ b/src/HOL/Tools/Function/mutual.ML	Sun May 09 15:28:44 2010 +0200
@@ -192,7 +192,7 @@
       (HOLogic.Trueprop $ HOLogic.mk_eq (list_comb (f, args), rhs))
       (fn _ => (Local_Defs.unfold_tac ctxt all_orig_fdefs)
          THEN EqSubst.eqsubst_tac ctxt [0] [simp] 1
-         THEN (simp_tac (simpset_of ctxt addsimps SumTree.proj_in_rules)) 1)
+         THEN (simp_tac (simpset_of ctxt)) 1) (* FIXME: global simpset?!! *)
     |> restore_cond
     |> export
   end
diff -r ef97c5006840 -r acb789f3936b src/HOL/Tools/Function/sum_tree.ML
--- a/src/HOL/Tools/Function/sum_tree.ML	Sun May 09 12:00:43 2010 +0200
+++ b/src/HOL/Tools/Function/sum_tree.ML	Sun May 09 15:28:44 2010 +0200
@@ -8,7 +8,6 @@
 struct
 
 (* Theory dependencies *)
-val proj_in_rules = [@{thm Projl_Inl}, @{thm Projr_Inr}]
 val sumcase_split_ss =
   HOL_basic_ss addsimps (@{thm Product_Type.split} :: @{thms sum.cases})