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  

     2.1 --- a/src/Pure/Isar/proof_context.ML	Mon Oct 25 19:24:43 1999 +0200
     2.2 +++ b/src/Pure/Isar/proof_context.ML	Mon Oct 25 20:38:03 1999 +0200
     2.3 @@ -40,10 +40,8 @@
     2.4    val auto_bind_facts: string -> term list -> context -> context
     2.5    val match_binds: (string list * string) list -> context -> context
     2.6    val match_binds_i: (term list * term) list -> context -> context
     2.7 -  val bind_propps: bool -> (string * (string list * string list)) list
     2.8 -    -> context -> context * term list
     2.9 -  val bind_propps_i: bool -> (term * (term list * term list)) list
    2.10 -    -> context -> context * term list
    2.11 +  val bind_propp: string * (string list * string list) -> context -> context * term
    2.12 +  val bind_propp_i: term * (term list * term list) -> context -> context * term
    2.13    val get_thm: context -> string -> thm
    2.14    val get_thms: context -> string -> thm list
    2.15    val get_thmss: context -> string list -> thm list
    2.16 @@ -529,7 +527,7 @@
    2.17    else
    2.18      (case Library.gen_rems (op =) (used2, used1) of
    2.19        [] => ()
    2.20 -    | extras => warning ("Introducing free type variables: " ^ commas extras));
    2.21 +    | extras => warning ("Introducing free type variables: " ^ commas (rev extras)));
    2.22  
    2.23  fun warn_extra_tfrees (ctxt1 as Context {defs = (_, _, used1), ...})
    2.24      (ctxt2 as Context {defs = (_, _, used2), ...}) = (warn_extra used1 used2; ctxt2);
    2.25 @@ -614,24 +612,14 @@
    2.26  
    2.27  (* bind proposition patterns *)
    2.28  
    2.29 -local
    2.30 -
    2.31 -fun gen_bind_propp prepp (ctxt, (raw_prop, (raw_pats1, raw_pats2))) =
    2.32 +fun gen_bind_propp prepp (raw_prop, (raw_pats1, raw_pats2)) ctxt =
    2.33    let
    2.34      val raw_pats = map (pair I) raw_pats1 @ map (pair Logic.strip_imp_concl) raw_pats2;
    2.35      val (ctxt', (pairs, prop)) = prep_declare_match prepp (ctxt, (raw_pats, raw_prop));
    2.36    in (ctxt' |> match_binds_i (map (apfst single) pairs), prop) end;
    2.37  
    2.38 -fun gen_bind_propps prepp warn args ctxt =
    2.39 -  apfst (if warn then warn_extra_tfrees ctxt else I)
    2.40 -    (foldl_map (gen_bind_propp prepp) (ctxt, args));
    2.41 -
    2.42 -in
    2.43 -
    2.44 -val bind_propps = gen_bind_propps (read_prop_pat, read_prop);
    2.45 -val bind_propps_i = gen_bind_propps (cert_prop_pat, cert_prop);
    2.46 -
    2.47 -end;
    2.48 +val bind_propp = gen_bind_propp (read_prop_pat, read_prop);
    2.49 +val bind_propp_i = gen_bind_propp (cert_prop_pat, cert_prop);
    2.50  
    2.51  
    2.52  
    2.53 @@ -699,7 +687,7 @@
    2.54  
    2.55  fun gen_assm prepp tac (ctxt, (name, attrs, raw_prop_pats)) =
    2.56    let
    2.57 -    val (ctxt', props) = prepp true raw_prop_pats ctxt;
    2.58 +    val (ctxt', props) = foldl_map (fn (c, x) => prepp x c) (ctxt, raw_prop_pats);
    2.59  
    2.60      val cprops = map (Thm.cterm_of (sign_of ctxt')) props;
    2.61      val cprops_tac = map (rpair tac) cprops;
    2.62 @@ -719,12 +707,12 @@
    2.63  
    2.64  fun gen_assms prepp tac args ctxt =
    2.65    let val (ctxt', thmss) = foldl_map (gen_assm prepp tac) (ctxt, args)
    2.66 -  in (ctxt', (thmss, prems_of ctxt')) end;
    2.67 +  in (warn_extra_tfrees ctxt ctxt', (thmss, prems_of ctxt')) end;
    2.68  
    2.69  in
    2.70  
    2.71 -val assume = gen_assms bind_propps;
    2.72 -val assume_i = gen_assms bind_propps_i;
    2.73 +val assume = gen_assms bind_propp;
    2.74 +val assume_i = gen_assms bind_propp_i;
    2.75  
    2.76  end;
    2.77