src/Pure/Isar/isar_thy.ML
changeset 7678 027b6ec2f084
parent 7666 226ea33c7cd6
child 7734 9c098c777926
     1.1 --- a/src/Pure/Isar/isar_thy.ML	Fri Oct 01 20:38:16 1999 +0200
     1.2 +++ b/src/Pure/Isar/isar_thy.ML	Fri Oct 01 20:38:50 1999 +0200
     1.3 @@ -135,6 +135,12 @@
     1.4      -> Toplevel.transition -> Toplevel.transition
     1.5    val finally_i: (thm list * Comment.interest) option * Comment.text
     1.6      -> Toplevel.transition -> Toplevel.transition
     1.7 +  val obtain: ((string list * string option) * Comment.text) list
     1.8 +    * ((string * Args.src list * (string * (string list * string list)) list)
     1.9 +      * Comment.text) list -> ProofHistory.T -> ProofHistory.T
    1.10 +  val obtain_i: ((string list * typ option) * Comment.text) list
    1.11 +    * ((string * Proof.context attribute list * (term * (term list * term list)) list)
    1.12 +      * Comment.text) list -> ProofHistory.T -> ProofHistory.T
    1.13    val use_mltext: string -> bool -> theory option -> unit
    1.14    val use_mltext_theory: string -> bool -> theory -> theory
    1.15    val use_setup: string -> theory -> theory
    1.16 @@ -281,6 +287,9 @@
    1.17  
    1.18  (* statements *)
    1.19  
    1.20 +fun multi_local_attribute state (name, src, s) =
    1.21 +  (name, map (Attrib.local_attribute (Proof.theory_of state)) src, s);
    1.22 +
    1.23  local
    1.24  
    1.25  fun global_statement f (name, src, s) int thy =
    1.26 @@ -296,8 +305,7 @@
    1.27  fun local_statement_i f g (name, atts, t) = ProofHistory.apply (f name atts t o g);
    1.28  
    1.29  fun multi_statement f args = ProofHistory.apply (fn state =>
    1.30 -  f (map (fn (name, src, s) =>
    1.31 -      (name, map (Attrib.local_attribute (Proof.theory_of state)) src, s)) args) state);
    1.32 +  f (map (multi_local_attribute state) args) state);
    1.33  
    1.34  fun multi_statement_i f args = ProofHistory.apply (f args);
    1.35  
    1.36 @@ -433,6 +441,17 @@
    1.37  end;
    1.38  
    1.39  
    1.40 +(* obtain *)
    1.41 +
    1.42 +fun obtain (xs, asms) = ProofHistory.applys (fn state =>
    1.43 +  Obtain.obtain (map Comment.ignore xs)
    1.44 +    (map (multi_local_attribute state o Comment.ignore) asms) state);
    1.45 +
    1.46 +fun obtain_i (xs, asms) = ProofHistory.applys
    1.47 +  (Obtain.obtain_i (map Comment.ignore xs) (map Comment.ignore asms));
    1.48 +
    1.49 +
    1.50 +
    1.51  (* use ML text *)
    1.52  
    1.53  fun use_mltext txt verb opt_thy = Context.setmp opt_thy (use_text verb) txt;