more accurate goal context;
authorwenzelm
Sat Nov 23 17:07:36 2013 +0100 (2013-11-23)
changeset 545665f3e9baa8f13
parent 54565 63e4474fd0ed
child 54567 cfe53047dc16
more accurate goal context;
src/HOL/Tools/Function/mutual.ML
src/Pure/Isar/expression.ML
     1.1 --- a/src/HOL/Tools/Function/mutual.ML	Sat Nov 23 17:07:11 2013 +0100
     1.2 +++ b/src/HOL/Tools/Function/mutual.ML	Sat Nov 23 17:07:36 2013 +0100
     1.3 @@ -187,8 +187,10 @@
     1.4        | [cond] => (Thm.implies_elim psimp (Thm.assume cond), Thm.implies_intr cond)
     1.5        | _ => raise General.Fail "Too many conditions"
     1.6  
     1.7 +    val (_, simp_ctxt) = ctxt
     1.8 +      |> Assumption.add_assumes (#hyps (Thm.crep_thm simp))
     1.9    in
    1.10 -    Goal.prove ctxt [] []
    1.11 +    Goal.prove simp_ctxt [] []
    1.12        (HOLogic.Trueprop $ HOLogic.mk_eq (list_comb (f, args), rhs))
    1.13        (fn _ =>
    1.14          Local_Defs.unfold_tac ctxt all_orig_fdefs
     2.1 --- a/src/Pure/Isar/expression.ML	Sat Nov 23 17:07:11 2013 +0100
     2.2 +++ b/src/Pure/Isar/expression.ML	Sat Nov 23 17:07:36 2013 +0100
     2.3 @@ -676,8 +676,11 @@
     2.4      val conjuncts =
     2.5        (Drule.equal_elim_rule2 OF [body_eq, rewrite_rule [pred_def] (Thm.assume (cert statement))])
     2.6        |> Conjunction.elim_balanced (length ts);
     2.7 +
     2.8 +    val (_, axioms_ctxt) = defs_ctxt
     2.9 +      |> Assumption.add_assumes (maps (#hyps o Thm.crep_thm) (defs @ conjuncts));
    2.10      val axioms = ts ~~ conjuncts |> map (fn (t, ax) =>
    2.11 -      Element.prove_witness defs_ctxt t
    2.12 +      Element.prove_witness axioms_ctxt t
    2.13         (rewrite_goals_tac defs THEN compose_tac (false, ax, 0) 1));
    2.14    in ((statement, intro, axioms), defs_thy) end;
    2.15