--- 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
--- 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})