1.1 --- a/src/Pure/Isar/proof.ML	Mon Oct 25 19:24:43 1999 +0200
     1.2 +++ b/src/Pure/Isar/proof.ML	Mon Oct 25 20:38:03 1999 +0200
     1.3 @@ -573,11 +573,11 @@
     1.4  
     1.5  fun setup_goal opt_block prepp kind after_qed name atts raw_propp state =
     1.6    let
     1.7 -    val (state', [prop]) =
     1.8 +    val (state', prop) =
     1.9        state
    1.10        |> assert_forward_or_chain
    1.11        |> enter_forward
    1.12 -      |> map_context_result (prepp [raw_propp]);
    1.13 +      |> map_context_result (prepp raw_propp);
    1.14      val cprop = Thm.cterm_of (sign_of state') prop;
    1.15      val goal = Drule.mk_triv_goal cprop;
    1.16    in
    1.17 @@ -593,22 +593,24 @@
    1.18  
    1.19  (*global goals*)
    1.20  fun global_goal prep kind name atts x thy =
    1.21 -  setup_goal I (prep false) kind Seq.single name atts x (init_state thy);
    1.22 +  setup_goal I prep kind Seq.single name atts x (init_state thy);
    1.23  
    1.24 -val theorem = global_goal ProofContext.bind_propps Theorem;
    1.25 -val theorem_i = global_goal ProofContext.bind_propps_i Theorem;
    1.26 -val lemma = global_goal ProofContext.bind_propps Lemma;
    1.27 -val lemma_i = global_goal ProofContext.bind_propps_i Lemma;
    1.28 +val theorem = global_goal ProofContext.bind_propp Theorem;
    1.29 +val theorem_i = global_goal ProofContext.bind_propp_i Theorem;
    1.30 +val lemma = global_goal ProofContext.bind_propp Lemma;
    1.31 +val lemma_i = global_goal ProofContext.bind_propp_i Lemma;
    1.32  
    1.33  
    1.34  (*local goals*)
    1.35 -fun local_goal prep kind f name atts x =
    1.36 -  setup_goal open_block (prep true) kind f name atts x;
    1.37 +fun local_goal prep kind f name atts args state =
    1.38 +  state
    1.39 +  |> setup_goal open_block prep kind f name atts args
    1.40 +  |> warn_extra_tfrees state;
    1.41  
    1.42 -val show   = local_goal ProofContext.bind_propps Goal;
    1.43 -val show_i = local_goal ProofContext.bind_propps_i Goal;
    1.44 -val have   = local_goal ProofContext.bind_propps Aux;
    1.45 -val have_i = local_goal ProofContext.bind_propps_i Aux;
    1.46 +val show   = local_goal ProofContext.bind_propp Goal;
    1.47 +val show_i = local_goal ProofContext.bind_propp_i Goal;
    1.48 +val have   = local_goal ProofContext.bind_propp Aux;
    1.49 +val have_i = local_goal ProofContext.bind_propp_i Aux;
    1.50  
    1.51  
    1.52