1.1 --- a/src/Pure/Isar/proof.ML	Thu Dec 22 00:29:06 2005 +0100
     1.2 +++ b/src/Pure/Isar/proof.ML	Thu Dec 22 00:29:07 2005 +0100
     1.3 @@ -403,7 +403,8 @@
     1.4        state
     1.5        |> check_theory (Thm.theory_of_thm goal')
     1.6        |> map_goal
     1.7 -          (ProofContext.add_cases (no_goal_cases goal @ goal_cases goal' @ meth_cases))
     1.8 +          (ProofContext.add_cases false (no_goal_cases goal @ goal_cases goal') #>
     1.9 +           ProofContext.add_cases true meth_cases)
    1.10            (K (statement, using, goal', before_qed, after_qed)))
    1.11    end;
    1.12  
    1.13 @@ -460,7 +461,7 @@
    1.14  
    1.15  (* conclude_goal *)
    1.16  
    1.17 -fun conclude_goal state props goal =
    1.18 +fun conclude_goal state goal props =
    1.19    let
    1.20      val ctxt = context_of state;
    1.21      fun err msg = raise STATE (msg, state);
    1.22 @@ -784,7 +785,7 @@
    1.23      |> tap (check_tvars props)
    1.24      |> tap (check_vars props)
    1.25      |> put_goal (SOME (make_goal ((kind, propss), [], goal, before_qed, after_qed')))
    1.26 -    |> map_context (ProofContext.add_cases (AutoBind.cases thy props))
    1.27 +    |> map_context (ProofContext.add_cases false (AutoBind.cases thy props))
    1.28      |> map_context (ProofContext.auto_bind_goal props)
    1.29      |> K chaining ? (`the_facts #-> using_facts)
    1.30      |> put_facts NONE
    1.31 @@ -805,7 +806,7 @@
    1.32      val props = ProofContext.generalize goal_ctxt outer_ctxt raw_props;
    1.33      val results =
    1.34        stmt
    1.35 -      |> burrow (fn raw_props => conclude_goal state raw_props goal)
    1.36 +      |> burrow (conclude_goal state goal)
    1.37        |> (Seq.map_list o Seq.map_list) (ProofContext.exports goal_ctxt outer_ctxt);
    1.38    in
    1.39      outer_state