assume: multiple args;

--- a/src/Pure/Isar/isar_thy.ML	Wed Aug 18 20:45:18 1999 +0200
+++ b/src/Pure/Isar/isar_thy.ML	Wed Aug 18 20:45:52 1999 +0200
@@ -83,14 +83,14 @@
     * Comment.text -> bool -> theory -> ProofHistory.T
   val lemma_i: (bstring * theory attribute list * (term * (term list * term list)))
     * Comment.text -> bool -> theory -> ProofHistory.T
-  val assume: (string * Args.src list * (string * (string list * string list)) list)
-    * Comment.text -> ProofHistory.T -> ProofHistory.T
-  val assume_i: (string * Proof.context attribute list * (term * (term list * term list)) list)
-    * Comment.text -> ProofHistory.T -> ProofHistory.T
-  val presume: (string * Args.src list * (string * (string list * string list)) list)
-    * Comment.text -> ProofHistory.T -> ProofHistory.T
-  val presume_i: (string * Proof.context attribute list * (term * (term list * term list)) list)
-    * Comment.text -> ProofHistory.T -> ProofHistory.T
+  val assume: ((string * Args.src list * (string * (string list * string list)) list)
+    * Comment.text) list -> ProofHistory.T -> ProofHistory.T
+  val assume_i: ((string * Proof.context attribute list * (term * (term list * term list)) list)
+    * Comment.text) list -> ProofHistory.T -> ProofHistory.T
+  val presume: ((string * Args.src list * (string * (string list * string list)) list)
+    * Comment.text) list -> ProofHistory.T -> ProofHistory.T
+  val presume_i: ((string * Proof.context attribute list * (term * (term list * term list)) list)
+    * Comment.text) list -> ProofHistory.T -> ProofHistory.T
   val local_def: (string * Args.src list * ((string * string option) * (string * string list)))
     * Comment.text -> ProofHistory.T -> ProofHistory.T
   val local_def_i: (string * Args.src list * ((string * typ) * (term * term list)))
@@ -273,6 +273,8 @@
 
 (* statements *)
 
+local
+
 fun global_statement f (name, src, s) int thy =
   ProofHistory.init (Toplevel.undo_limit int)
     (f name (map (Attrib.global_attribute thy) src) s thy);
@@ -285,14 +287,22 @@
 
 fun local_statement_i f g (name, atts, t) = ProofHistory.apply (f name atts t o g);
 
+fun multi_statement f args = ProofHistory.apply (fn state =>
+  f (map (fn (name, src, s) =>
+      (name, map (Attrib.local_attribute (Proof.theory_of state)) src, s)) args) state);
+
+fun multi_statement_i f args = ProofHistory.apply (f args);
+
+in
+
 val theorem     = global_statement Proof.theorem o Comment.ignore;
 val theorem_i   = global_statement_i Proof.theorem_i o Comment.ignore;
 val lemma       = global_statement Proof.lemma o Comment.ignore;
 val lemma_i     = global_statement_i Proof.lemma_i o Comment.ignore;
-val assume      = local_statement Proof.assume I o Comment.ignore;
-val assume_i    = local_statement_i Proof.assume_i I o Comment.ignore;
-val presume     = local_statement Proof.presume I o Comment.ignore;
-val presume_i   = local_statement_i Proof.presume_i I o Comment.ignore;
+val assume      = multi_statement Proof.assume o map Comment.ignore;
+val assume_i    = multi_statement_i Proof.assume_i o map Comment.ignore;
+val presume     = multi_statement Proof.presume o map Comment.ignore;
+val presume_i   = multi_statement_i Proof.presume_i o map Comment.ignore;
 val local_def   = local_statement LocalDefs.def I o Comment.ignore;
 val local_def_i = local_statement LocalDefs.def_i I o Comment.ignore;
 val show        = local_statement (Proof.show Seq.single) I o Comment.ignore;
@@ -304,6 +314,8 @@
 val hence       = local_statement (Proof.have Seq.single) Proof.chain o Comment.ignore;
 val hence_i     = local_statement_i (Proof.have_i Seq.single) Proof.chain o Comment.ignore;
 
+end;
+
 
 (* blocks *)
 

--- a/src/Pure/Isar/local_defs.ML	Wed Aug 18 20:45:18 1999 +0200
+++ b/src/Pure/Isar/local_defs.ML	Wed Aug 18 20:45:52 1999 +0200
@@ -39,7 +39,7 @@
     else ();
     state'
     |> match_binds [(raw_pats, raw_rhs)]   (*note: raw_rhs prepared twice!*)
-    |> Proof.assm_i (refl_tac, refl_tac) name atts [(eq, ([], []))]
+    |> Proof.assm_i (refl_tac, refl_tac) [(name, atts, [(eq, ([], []))])]
   end;
 
 val def = gen_def Proof.fix ProofContext.read_term Proof.match_bind;

--- a/src/Pure/Isar/proof.ML	Wed Aug 18 20:45:18 1999 +0200
+++ b/src/Pure/Isar/proof.ML	Wed Aug 18 20:45:52 1999 +0200
@@ -42,17 +42,19 @@
   val simple_have_thms: string -> thm list -> state -> state
   val fix: (string * string option) list -> state -> state
   val fix_i: (string * typ) list -> state -> state
-  val assm: (int -> tactic) * (int -> tactic) -> string -> context attribute list
-    -> (string * (string list * string list)) list -> state -> state
-  val assm_i: (int -> tactic) * (int -> tactic) -> string -> context attribute list
-    -> (term * (term list * term list)) list -> state -> state
-  val assume: string -> context attribute list -> (string * (string list * string list)) list
+  val assm: (int -> tactic) * (int -> tactic)
+    -> (string * context attribute list * (string * (string list * string list)) list) list
+    -> state -> state
+  val assm_i: (int -> tactic) * (int -> tactic)
+    -> (string * context attribute list * (term * (term list * term list)) list) list
     -> state -> state
-  val assume_i: string -> context attribute list -> (term * (term list * term list)) list
+  val assume: (string * context attribute list * (string * (string list * string list)) list) list
+    -> state -> state
+  val assume_i: (string * context attribute list * (term * (term list * term list)) list) list
     -> state -> state
-  val presume: string -> context attribute list -> (string * (string list * string list)) list
+  val presume: (string * context attribute list * (string * (string list * string list)) list) list
     -> state -> state
-  val presume_i: string -> context attribute list -> (term * (term list * term list)) list
+  val presume_i: (string * context attribute list * (term * (term list * term list)) list) list
     -> state -> state
   val theorem: bstring -> theory attribute list -> string * (string list * string list)
     -> theory -> state
@@ -526,26 +528,33 @@
 
 (* assume *)
 
-fun gen_assume f tacs name atts props state =
+local
+
+fun def_name (name, x, y) = (PureThy.default_name name, x, y);
+
+fun gen_assume f tac args state =
   state
   |> assert_forward
-  |> map_context_result (f tacs (PureThy.default_name name) atts props)
-  |> (fn (st, (facts, prems)) =>
-    (st, facts)
-    |> these_facts
-    |> put_thms ("prems", prems));
-
-val assm = gen_assume ProofContext.assume;
-val assm_i = gen_assume ProofContext.assume_i;
+  |> map_context_result (f tac (map def_name args))
+  |> (fn (st, (factss, prems)) =>
+    foldl these_facts (st, factss)
+    |> put_thms ("prems", prems)
+    |> put_facts (Some (flat (map #2 factss))));
 
 val hard_asm_tac = Tactic.etac Drule.triv_goal;
 val soft_asm_tac = Tactic.rtac Drule.triv_goal;
 
+in
+
+val assm = gen_assume ProofContext.assume;
+val assm_i = gen_assume ProofContext.assume_i;
 val assume = assm (hard_asm_tac, soft_asm_tac);
 val assume_i = assm_i (hard_asm_tac, soft_asm_tac);
 val presume = assm (soft_asm_tac, soft_asm_tac);
 val presume_i = assm_i (soft_asm_tac, soft_asm_tac);
 
+end;
+
 
 
 (** goals **)