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;