author | krauss |
Mon, 26 Mar 2007 16:35:33 +0200 | |
changeset 22526 | be2269950fe5 |
parent 22525 | d929a900584c |
child 22527 | 84690fcd3db9 |
--- a/src/HOL/Tools/function_package/mutual.ML Mon Mar 26 14:54:45 2007 +0200 +++ b/src/HOL/Tools/function_package/mutual.ML Mon Mar 26 16:35:33 2007 +0200 @@ -261,7 +261,7 @@ (HOLogic.Trueprop $ HOLogic.mk_eq (list_comb (f, args), rhs)) (fn _ => SIMPSET (unfold_tac all_orig_fdefs) THEN EqSubst.eqsubst_tac ctxt [0] [simp] 1 - THEN SIMPSET' simp_tac 1) + THEN SIMPSET' (fn ss => simp_tac (ss addsimps [@{thm "lproj_inl"}, @{thm "rproj_inr"}])) 1) |> restore_cond |> export end