# 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