do not redeclare [simp] rules, to avoid "duplicate rewrite rule" warnings
authorkrauss
Sun May 09 15:28:44 2010 +0200 (2010-05-09)
changeset 36773acb789f3936b
parent 36772 ef97c5006840
child 36775 ba2a7096dd2b
do not redeclare [simp] rules, to avoid "duplicate rewrite rule" warnings
src/HOL/Tools/Function/mutual.ML
src/HOL/Tools/Function/sum_tree.ML
     1.1 --- a/src/HOL/Tools/Function/mutual.ML	Sun May 09 12:00:43 2010 +0200
     1.2 +++ b/src/HOL/Tools/Function/mutual.ML	Sun May 09 15:28:44 2010 +0200
     1.3 @@ -192,7 +192,7 @@
     1.4        (HOLogic.Trueprop $ HOLogic.mk_eq (list_comb (f, args), rhs))
     1.5        (fn _ => (Local_Defs.unfold_tac ctxt all_orig_fdefs)
     1.6           THEN EqSubst.eqsubst_tac ctxt [0] [simp] 1
     1.7 -         THEN (simp_tac (simpset_of ctxt addsimps SumTree.proj_in_rules)) 1)
     1.8 +         THEN (simp_tac (simpset_of ctxt)) 1) (* FIXME: global simpset?!! *)
     1.9      |> restore_cond
    1.10      |> export
    1.11    end
     2.1 --- a/src/HOL/Tools/Function/sum_tree.ML	Sun May 09 12:00:43 2010 +0200
     2.2 +++ b/src/HOL/Tools/Function/sum_tree.ML	Sun May 09 15:28:44 2010 +0200
     2.3 @@ -8,7 +8,6 @@
     2.4  struct
     2.5  
     2.6  (* Theory dependencies *)
     2.7 -val proj_in_rules = [@{thm Projl_Inl}, @{thm Projr_Inr}]
     2.8  val sumcase_split_ss =
     2.9    HOL_basic_ss addsimps (@{thm Product_Type.split} :: @{thms sum.cases})
    2.10