src/HOL/Tools/function_package/mutual.ML

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