# HG changeset patch
# User wenzelm
# Date 940876683 -7200
# Node ID 06a11f8cf573f379eefcb70d401bd69d42ba129c
# Parent  b50446a33c160d805c6e4a3473978d4b39b067f4
improved handling of warn_extra_tfrees;

diff -r b50446a33c16 -r 06a11f8cf573 src/Pure/Isar/proof.ML
--- a/src/Pure/Isar/proof.ML	Mon Oct 25 19:24:43 1999 +0200
+++ b/src/Pure/Isar/proof.ML	Mon Oct 25 20:38:03 1999 +0200
@@ -573,11 +573,11 @@
 
 fun setup_goal opt_block prepp kind after_qed name atts raw_propp state =
   let
-    val (state', [prop]) =
+    val (state', prop) =
       state
       |> assert_forward_or_chain
       |> enter_forward
-      |> map_context_result (prepp [raw_propp]);
+      |> map_context_result (prepp raw_propp);
     val cprop = Thm.cterm_of (sign_of state') prop;
     val goal = Drule.mk_triv_goal cprop;
   in
@@ -593,22 +593,24 @@
 
 (*global goals*)
 fun global_goal prep kind name atts x thy =
-  setup_goal I (prep false) kind Seq.single name atts x (init_state thy);
+  setup_goal I prep kind Seq.single name atts x (init_state thy);
 
-val theorem = global_goal ProofContext.bind_propps Theorem;
-val theorem_i = global_goal ProofContext.bind_propps_i Theorem;
-val lemma = global_goal ProofContext.bind_propps Lemma;
-val lemma_i = global_goal ProofContext.bind_propps_i Lemma;
+val theorem = global_goal ProofContext.bind_propp Theorem;
+val theorem_i = global_goal ProofContext.bind_propp_i Theorem;
+val lemma = global_goal ProofContext.bind_propp Lemma;
+val lemma_i = global_goal ProofContext.bind_propp_i Lemma;
 
 
 (*local goals*)
-fun local_goal prep kind f name atts x =
-  setup_goal open_block (prep true) kind f name atts x;
+fun local_goal prep kind f name atts args state =
+  state
+  |> setup_goal open_block prep kind f name atts args
+  |> warn_extra_tfrees state;
 
-val show   = local_goal ProofContext.bind_propps Goal;
-val show_i = local_goal ProofContext.bind_propps_i Goal;
-val have   = local_goal ProofContext.bind_propps Aux;
-val have_i = local_goal ProofContext.bind_propps_i Aux;
+val show   = local_goal ProofContext.bind_propp Goal;
+val show_i = local_goal ProofContext.bind_propp_i Goal;
+val have   = local_goal ProofContext.bind_propp Aux;
+val have_i = local_goal ProofContext.bind_propp_i Aux;
 
 
 
diff -r b50446a33c16 -r 06a11f8cf573 src/Pure/Isar/proof_context.ML
--- a/src/Pure/Isar/proof_context.ML	Mon Oct 25 19:24:43 1999 +0200
+++ b/src/Pure/Isar/proof_context.ML	Mon Oct 25 20:38:03 1999 +0200
@@ -40,10 +40,8 @@
   val auto_bind_facts: string -> term list -> context -> context
   val match_binds: (string list * string) list -> context -> context
   val match_binds_i: (term list * term) list -> context -> context
-  val bind_propps: bool -> (string * (string list * string list)) list
-    -> context -> context * term list
-  val bind_propps_i: bool -> (term * (term list * term list)) list
-    -> context -> context * term list
+  val bind_propp: string * (string list * string list) -> context -> context * term
+  val bind_propp_i: term * (term list * term list) -> context -> context * term
   val get_thm: context -> string -> thm
   val get_thms: context -> string -> thm list
   val get_thmss: context -> string list -> thm list
@@ -529,7 +527,7 @@
   else
     (case Library.gen_rems (op =) (used2, used1) of
       [] => ()
-    | extras => warning ("Introducing free type variables: " ^ commas extras));
+    | extras => warning ("Introducing free type variables: " ^ commas (rev extras)));
 
 fun warn_extra_tfrees (ctxt1 as Context {defs = (_, _, used1), ...})
     (ctxt2 as Context {defs = (_, _, used2), ...}) = (warn_extra used1 used2; ctxt2);
@@ -614,24 +612,14 @@
 
 (* bind proposition patterns *)
 
-local
-
-fun gen_bind_propp prepp (ctxt, (raw_prop, (raw_pats1, raw_pats2))) =
+fun gen_bind_propp prepp (raw_prop, (raw_pats1, raw_pats2)) ctxt =
   let
     val raw_pats = map (pair I) raw_pats1 @ map (pair Logic.strip_imp_concl) raw_pats2;
     val (ctxt', (pairs, prop)) = prep_declare_match prepp (ctxt, (raw_pats, raw_prop));
   in (ctxt' |> match_binds_i (map (apfst single) pairs), prop) end;
 
-fun gen_bind_propps prepp warn args ctxt =
-  apfst (if warn then warn_extra_tfrees ctxt else I)
-    (foldl_map (gen_bind_propp prepp) (ctxt, args));
-
-in
-
-val bind_propps = gen_bind_propps (read_prop_pat, read_prop);
-val bind_propps_i = gen_bind_propps (cert_prop_pat, cert_prop);
-
-end;
+val bind_propp = gen_bind_propp (read_prop_pat, read_prop);
+val bind_propp_i = gen_bind_propp (cert_prop_pat, cert_prop);
 
 
 
@@ -699,7 +687,7 @@
 
 fun gen_assm prepp tac (ctxt, (name, attrs, raw_prop_pats)) =
   let
-    val (ctxt', props) = prepp true raw_prop_pats ctxt;
+    val (ctxt', props) = foldl_map (fn (c, x) => prepp x c) (ctxt, raw_prop_pats);
 
     val cprops = map (Thm.cterm_of (sign_of ctxt')) props;
     val cprops_tac = map (rpair tac) cprops;
@@ -719,12 +707,12 @@
 
 fun gen_assms prepp tac args ctxt =
   let val (ctxt', thmss) = foldl_map (gen_assm prepp tac) (ctxt, args)
-  in (ctxt', (thmss, prems_of ctxt')) end;
+  in (warn_extra_tfrees ctxt ctxt', (thmss, prems_of ctxt')) end;
 
 in
 
-val assume = gen_assms bind_propps;
-val assume_i = gen_assms bind_propps_i;
+val assume = gen_assms bind_propp;
+val assume_i = gen_assms bind_propp_i;
 
 end;