1.1 --- a/src/Pure/Isar/proof.ML	Mon Apr 26 16:08:04 2010 +0200
     1.2 +++ b/src/Pure/Isar/proof.ML	Mon Apr 26 20:30:50 2010 +0200
     1.3 @@ -792,7 +792,7 @@
     1.4  
     1.5  fun implicit_vars props =
     1.6    let
     1.7 -    val (var_props, props') = take_prefix is_var props;
     1.8 +    val (var_props, _) = take_prefix is_var props;
     1.9      val explicit_vars = fold Term.add_vars var_props [];
    1.10      val vars = filter_out (member (op =) explicit_vars) (fold Term.add_vars props []);
    1.11    in map (Logic.mk_term o Var) vars end;
    1.12 @@ -845,11 +845,10 @@
    1.13  
    1.14  fun generic_qed after_ctxt state =
    1.15    let
    1.16 -    val (goal_ctxt, {statement, goal, after_qed, ...}) = current_goal state;
    1.17 +    val (goal_ctxt, {statement = (_, stmt, _), goal, after_qed, ...}) = current_goal state;
    1.18      val outer_state = state |> close_block;
    1.19      val outer_ctxt = context_of outer_state;
    1.20  
    1.21 -    val ((_, pos), stmt, _) = statement;
    1.22      val props =
    1.23        flat (tl stmt)
    1.24        |> Variable.exportT_terms goal_ctxt outer_ctxt;