--- a/src/HOL/Tools/Function/mutual.ML Sun Aug 16 18:19:30 2015 +0200
+++ b/src/HOL/Tools/Function/mutual.ML Sun Aug 16 19:25:08 2015 +0200
@@ -182,7 +182,7 @@
| [cond] => (Thm.implies_elim psimp (Thm.assume cond), Thm.implies_intr cond)
| _ => raise General.Fail "Too many conditions"
- val simp_ctxt = fold Thm.declare_hyps (#hyps (Thm.crep_thm simp)) ctxt
+ val simp_ctxt = fold Thm.declare_hyps (Thm.chyps_of simp) ctxt
in
Goal.prove simp_ctxt [] []
(HOLogic.Trueprop $ HOLogic.mk_eq (list_comb (f, args), rhs))