improved source arrangement of obtain;

--- a/src/Pure/Isar/isar_syn.ML	Mon Oct 22 18:02:21 2001 +0200
+++ b/src/Pure/Isar/isar_syn.ML	Mon Oct 22 18:02:50 2001 +0200
@@ -338,6 +338,11 @@
 
 (* proof context *)
 
+val fixP =
+  OuterSyntax.command "fix" "fix variables (Skolem constants)" K.prf_asm
+    (P.and_list1 (Scan.repeat1 P.name -- Scan.option (P.$$$ "::" |-- P.typ) -- P.marg_comment)
+      >> (Toplevel.print oo (Toplevel.proof o IsarThy.fix)));
+
 val assumeP =
   OuterSyntax.command "assume" "assume propositions" K.prf_asm
     (P.and_list1 (P.opt_thm_name ":" -- Scan.repeat1 P.propp -- P.marg_comment)
@@ -353,10 +358,14 @@
     (P.opt_thm_name ":" -- (P.name -- ((P.$$$ "\\<equiv>" || P.$$$ "==") |-- P.!!! P.termp))
       -- P.marg_comment >> (Toplevel.print oo (Toplevel.proof o IsarThy.local_def)));
 
-val fixP =
-  OuterSyntax.command "fix" "fix variables (Skolem constants)" K.prf_asm
-    (P.and_list1 (Scan.repeat1 P.name -- Scan.option (P.$$$ "::" |-- P.typ) -- P.marg_comment)
-      >> (Toplevel.print oo (Toplevel.proof o IsarThy.fix)));
+val obtainP =
+  OuterSyntax.command "obtain" "generalized existence"
+    K.prf_asm_goal
+    (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.marg_comment)
+    >> (Toplevel.print oo (Toplevel.proof o IsarThy.obtain)));
 
 val letP =
   OuterSyntax.command "let" "bind text variables" K.prf_decl
@@ -689,7 +698,7 @@
  ["!", "!!", "%", "%%", "(", ")", "+", ",", "--", ":", "::", ";", "<",
   "<=", "=", "==", "=>", "?", "[", "]", "and", "binder", "concl",
   "files", "in", "infix", "infixl", "infixr", "is", "output", "overloaded",
-  "|", "\\<equiv>", "\\<rightharpoonup>", "\\<leftharpoondown>",
+  "where", "|", "\\<equiv>", "\\<rightharpoonup>", "\\<leftharpoondown>",
   "\\<rightleftharpoons>", "\\<subseteq>"];
 
 val parsers = [
@@ -707,9 +716,9 @@
   typed_print_translationP, print_ast_translationP,
   token_translationP, oracleP,
   (*proof commands*)
-  theoremP, lemmaP, corollaryP, showP, haveP, thusP, henceP, assumeP,
-  presumeP, defP, fixP, letP, caseP, thenP, fromP, withP, noteP,
-  beginP, endP, nextP, qedP, terminal_proofP, default_proofP,
+  theoremP, lemmaP, corollaryP, showP, haveP, thusP, henceP, fixP,
+  assumeP, presumeP, defP, obtainP, letP, caseP, thenP, fromP, withP,
+  noteP, beginP, endP, nextP, qedP, terminal_proofP, default_proofP,
   immediate_proofP, done_proofP, skip_proofP, forget_proofP, deferP,
   preferP, applyP, apply_endP, proofP, alsoP, finallyP, moreoverP,
   ultimatelyP, backP, cannot_undoP, clear_undosP, redoP, undos_proofP,

--- a/src/Pure/Isar/isar_thy.ML	Mon Oct 22 18:02:21 2001 +0200
+++ b/src/Pure/Isar/isar_thy.ML	Mon Oct 22 18:02:50 2001 +0200
@@ -123,6 +123,12 @@
     * Comment.text -> ProofHistory.T -> ProofHistory.T
   val hence_i: ((string * Proof.context attribute list) * (term * (term list * term list)))
     * Comment.text -> ProofHistory.T -> ProofHistory.T
+  val obtain: ((string list * string option) * Comment.text) 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)
+      * Comment.text) list -> ProofHistory.T -> ProofHistory.T
   val begin_block: Comment.text -> ProofHistory.T -> ProofHistory.T
   val next_block: Comment.text -> ProofHistory.T -> ProofHistory.T
   val end_block: Comment.text -> ProofHistory.T -> ProofHistory.T
@@ -424,8 +430,8 @@
 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 local_def   = local_statement Proof.def I o Comment.ignore;
+val local_def_i = local_statement Proof.def_i I o Comment.ignore;
 val show        = local_statement' (Proof.show check_goal Seq.single) I o Comment.ignore;
 val show_i      = local_statement_i' (Proof.show_i check_goal Seq.single) I o Comment.ignore;
 val have        = local_statement (Proof.have Seq.single) I o Comment.ignore;
@@ -435,6 +441,13 @@
 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;
 
+fun obtain (xs, asms) = ProofHistory.applys (fn state =>
+  Obtain.obtain (map Comment.ignore xs)
+    (map (multi_local_attribute state) (map Comment.ignore asms)) state);
+
+fun obtain_i (xs, asms) = ProofHistory.applys (fn state =>
+  Obtain.obtain_i (map Comment.ignore xs) (map Comment.ignore asms) state);
+
 end;
 
 

--- a/src/Pure/Isar/obtain.ML	Mon Oct 22 18:02:21 2001 +0200
+++ b/src/Pure/Isar/obtain.ML	Mon Oct 22 18:02:50 2001 +0200
@@ -20,12 +20,12 @@
 
 signature OBTAIN =
 sig
-  val obtain: ((string list * string option) * Comment.text) 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)
-      * Comment.text) list -> ProofHistory.T -> ProofHistory.T
+  val obtain: (string list * string option) list ->
+    ((string * Proof.context attribute list) * (string * (string list * string list)) list) list
+    -> Proof.state -> Proof.state Seq.seq
+  val obtain_i: (string list * typ option) list ->
+    ((string * Proof.context attribute list) * (term * (term list * term list)) list) list
+    -> Proof.state -> Proof.state Seq.seq
 end;
 
 structure Obtain: OBTAIN =
@@ -62,7 +62,7 @@
 
 val thatN = "that";
 
-fun gen_obtain prep_vars prep_propp prep_att (raw_vars, raw_asms) state =
+fun gen_obtain prep_vars prep_propp raw_vars raw_asms state =
   let
     val _ = Proof.assert_forward_or_chain state;
     val chain_facts = if Proof.is_chain state then Proof.the_facts state else [];
@@ -70,17 +70,14 @@
     val sign = Theory.sign_of thy;
 
     (*obtain vars*)
-    val (vars_ctxt, vars) =
-      foldl_map prep_vars (Proof.context_of state, map Comment.ignore raw_vars);
+    val (vars_ctxt, vars) = foldl_map prep_vars (Proof.context_of state, raw_vars);
     val xs = flat (map fst vars);
     val fix_ctxt = vars_ctxt |> ProofContext.fix_i vars;
 
     (*obtain asms*)
-    val (asms_ctxt, proppss) = prep_propp (fix_ctxt, map (snd o Comment.ignore) raw_asms);
+    val (asms_ctxt, proppss) = prep_propp (fix_ctxt, map snd raw_asms);
     val asm_props = flat (map (map fst) proppss);
-
-    fun prep_asm ((name, src), propps) = ((name, map (prep_att thy) src), propps);
-    val asms = map2 prep_asm (map (fst o Comment.ignore) raw_asms, proppss);
+    val asms = map fst raw_asms ~~ proppss;
 
     val _ = ProofContext.warn_extra_tfrees fix_ctxt asms_ctxt;
 
@@ -118,31 +115,8 @@
       |> Method.refine (Method.Basic (K (Method.insert (Proof.the_facts state')))))
   end;
 
-
-val obtain = ProofHistory.applys o
-  (gen_obtain ProofContext.read_vars ProofContext.read_propp Attrib.local_attribute);
-
-val obtain_i = ProofHistory.applys o
-  (gen_obtain ProofContext.cert_vars ProofContext.cert_propp (K I));
-
+val obtain = gen_obtain ProofContext.read_vars ProofContext.read_propp;
+val obtain_i = gen_obtain ProofContext.cert_vars ProofContext.cert_propp;
 
 
-(** outer syntax **)
-
-local structure P = OuterParse and K = OuterSyntax.Keyword in
-
-val obtainP =
-  OuterSyntax.command "obtain" "generalized existence"
-    K.prf_asm_goal
-    (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.marg_comment)
-    >> (Toplevel.print oo (Toplevel.proof o obtain)));
-
-val _ = OuterSyntax.add_keywords ["where"];
-val _ = OuterSyntax.add_parsers [obtainP];
-
 end;
-
-end;