# HG changeset patch
# User wenzelm
# Date 974149267 -3600
# Node ID b7b916a82dca6af8ae6523ff9841b8620c08f983
# Parent  474263d290576c42bb7b64a595b531842e645068
tuned statement args;

diff -r 474263d29057 -r b7b916a82dca src/Pure/Isar/isar_syn.ML
--- a/src/Pure/Isar/isar_syn.ML	Mon Nov 13 21:59:49 2000 +0100
+++ b/src/Pure/Isar/isar_syn.ML	Mon Nov 13 22:01:07 2000 +0100
@@ -283,7 +283,7 @@
 
 (* statements *)
 
-fun statement f = (P.opt_thm_name ":" -- P.propp >> P.triple1) -- P.marg_comment >> f;
+fun statement f = P.opt_thm_name ":" -- P.propp -- P.marg_comment >> f;
 
 val theoremP =
   OuterSyntax.command "theorem" "state theorem" K.thy_goal
@@ -335,17 +335,17 @@
 
 val assumeP =
   OuterSyntax.command "assume" "assume propositions" K.prf_asm
-    (P.and_list1 ((P.opt_thm_name ":" -- Scan.repeat1 P.propp >> P.triple1) -- P.marg_comment)
+    (P.and_list1 (P.opt_thm_name ":" -- Scan.repeat1 P.propp -- P.marg_comment)
       >> (Toplevel.print oo (Toplevel.proof o IsarThy.assume)));
 
 val presumeP =
   OuterSyntax.command "presume" "assume propositions, to be established later" K.prf_asm
-    (P.and_list1 ((P.opt_thm_name ":" -- Scan.repeat1 P.propp >> P.triple1) -- P.marg_comment)
+    (P.and_list1 (P.opt_thm_name ":" -- Scan.repeat1 P.propp -- P.marg_comment)
       >> (Toplevel.print oo (Toplevel.proof o IsarThy.presume)));
 
 val defP =
   OuterSyntax.command "def" "local definition" K.prf_asm
-    ((P.opt_thm_name ":" -- (P.name -- (P.$$$ "==" |-- P.!!! P.termp)) >> P.triple1)
+    (P.opt_thm_name ":" -- (P.name -- (P.$$$ "==" |-- P.!!! P.termp))
       -- P.marg_comment >> (Toplevel.print oo (Toplevel.proof o IsarThy.local_def)));
 
 val fixP =
diff -r 474263d29057 -r b7b916a82dca src/Pure/Isar/isar_thy.ML
--- a/src/Pure/Isar/isar_thy.ML	Mon Nov 13 21:59:49 2000 +0100
+++ b/src/Pure/Isar/isar_thy.ML	Mon Nov 13 22:01:07 2000 +0100
@@ -63,22 +63,27 @@
   val apply_theorems_i: (thm * theory attribute list) list -> theory -> theory * thm list
   val declare_theorems: (xstring * Args.src list) list * Comment.text -> theory -> theory
   val declare_theorems_i: (thm * theory attribute list) list * Comment.text -> theory -> theory
-  val have_theorems: (((bstring * Args.src list) * (xstring * Args.src list) list) * Comment.text) list
+  val have_theorems:
+    (((bstring * Args.src list) * (xstring * Args.src list) list) * Comment.text) list
     -> theory -> theory
   val have_theorems_i: (((bstring * theory attribute list) * (thm * theory attribute list) list)
     * Comment.text) list -> theory -> theory
-  val have_lemmas: (((bstring * Args.src list) * (xstring * Args.src list) list) * Comment.text) list
+  val have_lemmas:
+    (((bstring * Args.src list) * (xstring * Args.src list) list) * Comment.text) list
     -> theory -> theory
   val have_lemmas_i: (((bstring * theory attribute list) * (thm * theory attribute list) list)
     * Comment.text) list -> theory -> theory
   val have_facts: (((string * Args.src list) * (string * Args.src list) list) * Comment.text) list
     -> ProofHistory.T -> ProofHistory.T
   val have_facts_i: (((string * Proof.context attribute list) *
-    (thm * Proof.context attribute list) list) * Comment.text) list -> ProofHistory.T -> ProofHistory.T
-  val from_facts: ((string * Args.src list) list * Comment.text) list -> ProofHistory.T -> ProofHistory.T
+    (thm * Proof.context attribute list) list) * Comment.text) list
+    -> ProofHistory.T -> ProofHistory.T
+  val from_facts: ((string * Args.src list) list * Comment.text) list
+    -> ProofHistory.T -> ProofHistory.T
   val from_facts_i: ((thm * Proof.context attribute list) list * Comment.text) list
     -> ProofHistory.T -> ProofHistory.T
-  val with_facts: ((string * Args.src list) list * Comment.text) list -> ProofHistory.T -> ProofHistory.T
+  val with_facts: ((string * Args.src list) list * Comment.text) list
+    -> ProofHistory.T -> ProofHistory.T
   val with_facts_i: ((thm * Proof.context attribute list) list * Comment.text) list
     -> ProofHistory.T -> ProofHistory.T
   val chain: Comment.text -> ProofHistory.T -> ProofHistory.T
@@ -89,41 +94,41 @@
   val invoke_case: (string * Args.src list) * Comment.text -> ProofHistory.T -> ProofHistory.T
   val invoke_case_i: (string * Proof.context attribute list) * Comment.text
     -> ProofHistory.T -> ProofHistory.T
-  val theorem: (bstring * Args.src list * (string * (string list * string list)))
+  val theorem: ((bstring * Args.src list) * (string * (string list * string list)))
     * Comment.text -> bool -> theory -> ProofHistory.T
-  val theorem_i: (bstring * theory attribute list * (term * (term list * term list)))
+  val theorem_i: ((bstring * theory attribute list) * (term * (term list * term list)))
     * Comment.text -> bool -> theory -> ProofHistory.T
-  val lemma: (bstring * Args.src list * (string * (string list * string list)))
+  val lemma: ((bstring * Args.src list) * (string * (string list * string list)))
     * Comment.text -> bool -> theory -> ProofHistory.T
-  val lemma_i: (bstring * theory attribute list * (term * (term list * term list)))
+  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)
+  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)
+  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)
+  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)
+  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 * string list)))
+  val local_def: ((string * Args.src list) * (string * (string * string list)))
     * Comment.text -> ProofHistory.T -> ProofHistory.T
-  val local_def_i: (string * Args.src list * (string * (term * term list)))
+  val local_def_i: ((string * Args.src list) * (string * (term * term list)))
     * Comment.text -> ProofHistory.T -> ProofHistory.T
-  val show: (string * Args.src list * (string * (string list * string list)))
+  val show: ((string * Args.src list) * (string * (string list * string list)))
     * Comment.text -> ProofHistory.T -> ProofHistory.T
-  val show_i: (string * Proof.context attribute list * (term * (term list * term list)))
+  val show_i: ((string * Proof.context attribute list) * (term * (term list * term list)))
     * Comment.text -> ProofHistory.T -> ProofHistory.T
-  val have: (string * Args.src list * (string * (string list * string list)))
+  val have: ((string * Args.src list) * (string * (string list * string list)))
     * Comment.text -> ProofHistory.T -> ProofHistory.T
-  val have_i: (string * Proof.context attribute list * (term * (term list * term list)))
+  val have_i: ((string * Proof.context attribute list) * (term * (term list * term list)))
     * Comment.text -> ProofHistory.T -> ProofHistory.T
-  val thus: (string * Args.src list * (string * (string list * string list)))
+  val thus: ((string * Args.src list) * (string * (string list * string list)))
     * Comment.text -> ProofHistory.T -> ProofHistory.T
-  val thus_i: (string * Proof.context attribute list * (term * (term list * term list)))
+  val thus_i: ((string * Proof.context attribute list) * (term * (term list * term list)))
     * Comment.text -> ProofHistory.T -> ProofHistory.T
-  val hence: (string * Args.src list * (string * (string list * string list)))
+  val hence: ((string * Args.src list) * (string * (string list * string list)))
     * Comment.text -> ProofHistory.T -> ProofHistory.T
-  val hence_i: (string * Proof.context attribute list * (term * (term list * term list)))
+  val hence_i: ((string * Proof.context attribute list) * (term * (term list * term list)))
     * Comment.text -> ProofHistory.T -> ProofHistory.T
   val begin_block: Comment.text -> ProofHistory.T -> ProofHistory.T
   val next_block: Comment.text -> ProofHistory.T -> ProofHistory.T
@@ -358,20 +363,20 @@
 
 local
 
-fun global_statement f (name, src, s) int thy =
+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);
 
-fun global_statement_i f (name, atts, t) int thy =
+fun global_statement_i f ((name, atts), t) int thy =
   ProofHistory.init (Toplevel.undo_limit int) (f name atts t thy);
 
-fun local_statement f g (name, src, s) = ProofHistory.apply (fn state =>
+fun local_statement f g ((name, src), s) = ProofHistory.apply (fn state =>
   f name (map (Attrib.local_attribute (Proof.theory_of state)) src) s (g state));
 
-fun local_statement_i f g (name, atts, t) = ProofHistory.apply (f name atts t o g);
+fun local_statement_i f g ((name, atts), t) = ProofHistory.apply (f name atts t o g);
 
-fun multi_local_attribute state (name, src, s) =
-  (name, map (Attrib.local_attribute (Proof.theory_of state)) src, s);
+fun multi_local_attribute state ((name, src), s) =
+  ((name, map (Attrib.local_attribute (Proof.theory_of state)) src), s);
 
 fun multi_statement f args = ProofHistory.apply (fn state =>
   f (map (multi_local_attribute state) args) state);
diff -r 474263d29057 -r b7b916a82dca src/Pure/Isar/local_defs.ML
--- a/src/Pure/Isar/local_defs.ML	Mon Nov 13 21:59:49 2000 +0100
+++ b/src/Pure/Isar/local_defs.ML	Mon Nov 13 22:01:07 2000 +0100
@@ -63,7 +63,7 @@
     state
     |> fix [([x], None)]
     |> Proof.match_bind_i [(pats, rhs)]
-    |> Proof.assm_i export_defs [(name, atts, [(Logic.mk_equals (lhs, rhs), ([], []))])]
+    |> Proof.assm_i export_defs [((name, atts), [(Logic.mk_equals (lhs, rhs), ([], []))])]
   end;
 
 val def = gen_def Proof.fix ProofContext.read_term ProofContext.read_term_pats;
diff -r 474263d29057 -r b7b916a82dca src/Pure/Isar/obtain.ML
--- a/src/Pure/Isar/obtain.ML	Mon Nov 13 21:59:49 2000 +0100
+++ b/src/Pure/Isar/obtain.ML	Mon Nov 13 22:01:07 2000 +0100
@@ -21,10 +21,10 @@
 signature OBTAIN =
 sig
   val obtain: ((string list * string option) * Comment.text) list
-    * ((string * Args.src list * (string * (string list * string list)) list)
+    * (((string * Args.src list) * (string * (string list * string list)) list)
       * Comment.text) list -> ProofHistory.T -> ProofHistory.T
   val obtain_i: ((string list * typ option) * Comment.text) list
-    * ((string * Proof.context attribute list * (term * (term list * term list)) list)
+    * (((string * Proof.context attribute list) * (term * (term list * term list)) list)
       * Comment.text) list -> ProofHistory.T -> ProofHistory.T
 end;
 
@@ -66,6 +66,7 @@
   let
     val _ = Proof.assert_forward_or_chain state;
     val chain_facts = if Proof.is_chain state then Proof.the_facts state else [];
+    val thy = Proof.theory_of state;
 
     (*obtain vars*)
     val (vars_ctxt, vars) =
@@ -78,15 +79,12 @@
       (bind_skolem prop, (map bind_skolem pats1, map bind_skolem pats2));
 
     (*obtain asms*)
-    fun prep_asm (ctxt, (name, src, raw_propps)) =
-      let
-        val atts = map (prep_att (ProofContext.theory_of ctxt)) src;
-        val (ctxt', propps) = foldl_map prep_propp (ctxt, raw_propps);
-      in (ctxt', ((name, atts, map bind_propp propps), map #1 propps)) end;
+    val (asms_ctxt, proppss) = prep_propp (vars_ctxt, map (snd o Comment.ignore) raw_asms);
+    val asm_props = flat (map (map fst) proppss);
 
-    val (asms_ctxt, asms_result) = foldl_map prep_asm (vars_ctxt, map Comment.ignore raw_asms);
-    val (asms, asm_propss) = Library.split_list asms_result;
-    val asm_props = flat asm_propss;
+    fun prep_asm ((name, src), propps) = ((name, map (prep_att thy) src), map bind_propp propps);
+    val asms = map2 prep_asm (map (fst o Comment.ignore) raw_asms, proppss);
+
     val _ = ProofContext.warn_extra_tfrees vars_ctxt asms_ctxt;
 
     (*that_prop*)
@@ -96,7 +94,7 @@
     val xs' = mapfilter occs_var xs;
     val parms = map (bind_skolem o Free) xs';
 
-    val bound_thesis = bind_skolem (AutoBind.atomic_judgment (Proof.theory_of state) thesisN);
+    val bound_thesis = bind_skolem (AutoBind.atomic_judgment thy thesisN);
     val that_prop = Term.list_all_free (xs', Logic.list_implies (asm_props, bound_thesis));
 
     fun export_obtained rule =
@@ -112,7 +110,7 @@
     |> Proof.enter_forward
     |> Proof.begin_block
     |> Proof.fix_i [([thesisN], None)]
-    |> Proof.assume_i [(thatN, [Method.intro_local], [(that_prop, ([], []))])]
+    |> Proof.assume_i [((thatN, [Method.intro_local]), [(that_prop, ([], []))])]
     |> (fn state' =>
       state'
       |> Proof.from_facts chain_facts
@@ -139,7 +137,7 @@
     (Scan.optional
       (P.and_list1 (Scan.repeat1 P.name -- Scan.option (P.$$$ "::" |-- P.typ) -- P.marg_comment)
         --| P.$$$ "where") [] --
-      P.and_list1 ((P.opt_thm_name ":" -- Scan.repeat1 P.propp >> P.triple1) -- P.marg_comment)
+      P.and_list1 (P.opt_thm_name ":" -- Scan.repeat1 P.propp -- P.marg_comment)
     >> (Toplevel.print oo (Toplevel.proof o obtain)));
 
 val _ = OuterSyntax.add_keywords ["where"];
diff -r 474263d29057 -r b7b916a82dca src/Pure/Isar/proof.ML
--- a/src/Pure/Isar/proof.ML	Mon Nov 13 21:59:49 2000 +0100
+++ b/src/Pure/Isar/proof.ML	Mon Nov 13 22:01:07 2000 +0100
@@ -66,18 +66,20 @@
   val hard_asm_tac: int -> tactic
   val soft_asm_tac: int -> tactic
   val assm: ProofContext.exporter
-    -> (string * context attribute list * (string * (string list * string list)) list) list
+    -> ((string * context attribute list) * (string * (string list * string list)) list) list
     -> state -> state
   val assm_i: ProofContext.exporter
-    -> (string * context attribute list * (term * (term list * term list)) list) list
+    -> ((string * context attribute list) * (term * (term list * term list)) list) list
     -> state -> state
-  val assume: (string * context attribute list * (string * (string list * string list)) 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
+  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) 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) list
+  val presume_i: ((string * context attribute list) * (term * (term list * term list)) list) list
     -> state -> state
   val invoke_case: string * context attribute list -> state -> state
   val theorem: bstring -> theory attribute list -> string * (string list * string list)
@@ -555,7 +557,7 @@
   in
     state
     |> fix_i (map (fn (x, T) => ([x], Some T)) vars)
-    |> assume_i [(name, atts, map (fn t => (t, ([], []))) (map bind_skolem props))]
+    |> assume_i [((name, atts), map (fn t => (t, ([], []))) (map bind_skolem props))]
   end;
 
 
@@ -582,12 +584,12 @@
 
 fun setup_goal opt_block prepp kind after_qed name atts raw_propp state =
   let
-    val (state', (prop, gen_binds)) =
+    val (state', ([[prop]], gen_binds)) =
       state
       |> assert_forward_or_chain
       |> enter_forward
       |> opt_block
-      |> map_context_result (fn ct => prepp (ct, raw_propp));
+      |> map_context_result (fn ct => prepp (ct, [[raw_propp]]));
     val cprop = Thm.cterm_of (sign_of state') prop;
     val goal = Drule.mk_triv_goal cprop;
   in