--- a/src/HOL/Tools/Function/mutual.ML Sat Nov 23 17:07:11 2013 +0100
+++ b/src/HOL/Tools/Function/mutual.ML Sat Nov 23 17:07:36 2013 +0100
@@ -187,8 +187,10 @@
| [cond] => (Thm.implies_elim psimp (Thm.assume cond), Thm.implies_intr cond)
| _ => raise General.Fail "Too many conditions"
+ val (_, simp_ctxt) = ctxt
+ |> Assumption.add_assumes (#hyps (Thm.crep_thm simp))
in
- Goal.prove ctxt [] []
+ Goal.prove simp_ctxt [] []
(HOLogic.Trueprop $ HOLogic.mk_eq (list_comb (f, args), rhs))
(fn _ =>
Local_Defs.unfold_tac ctxt all_orig_fdefs