# HG changeset patch
# User krauss
# Date 1174919733 -7200
# Node ID be2269950fe56e7a0eb4264ea7fb9a1b27fd06e4
# Parent  d929a900584cfd99bffe71a05db8b889c3adf863
fixed problem with mutual recursion

diff -r d929a900584c -r be2269950fe5 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