src/Pure/Isar/isar_thy.ML
changeset 8450 dc44d6533f0f
parent 8428 be4c8a57cf7e
child 8466 f7b06595d0c8
     1.1 --- a/src/Pure/Isar/isar_thy.ML	Tue Mar 14 11:32:38 2000 +0100
     1.2 +++ b/src/Pure/Isar/isar_thy.ML	Tue Mar 14 11:33:14 2000 +0100
     1.3 @@ -79,7 +79,9 @@
     1.4    val fix_i: ((string list * typ option) * Comment.text) list -> ProofHistory.T -> ProofHistory.T
     1.5    val match_bind: ((string list * string) * Comment.text) list -> ProofHistory.T -> ProofHistory.T
     1.6    val match_bind_i: ((term list * term) * Comment.text) list -> ProofHistory.T -> ProofHistory.T
     1.7 -  val invoke_case: string * Comment.text -> ProofHistory.T -> ProofHistory.T
     1.8 +  val invoke_case: (string * Args.src list) * Comment.text -> ProofHistory.T -> ProofHistory.T
     1.9 +  val invoke_case_i: (string * Proof.context attribute list) * Comment.text
    1.10 +    -> ProofHistory.T -> ProofHistory.T
    1.11    val theorem: (bstring * Args.src list * (string * (string list * string list)))
    1.12      * Comment.text -> bool -> theory -> ProofHistory.T
    1.13    val theorem_i: (bstring * theory attribute list * (term * (term list * term list)))
    1.14 @@ -288,7 +290,10 @@
    1.15  val fix_i = ProofHistory.apply o Proof.fix_i o map Comment.ignore;
    1.16  val match_bind = ProofHistory.apply o Proof.match_bind o map Comment.ignore;
    1.17  val match_bind_i = ProofHistory.apply o Proof.match_bind_i o map Comment.ignore;
    1.18 -val invoke_case = ProofHistory.apply o Proof.invoke_case o Comment.ignore;
    1.19 +
    1.20 +fun invoke_case ((name, src), comment_ignore) = ProofHistory.apply (fn state =>
    1.21 +  Proof.invoke_case (name, map (Attrib.local_attribute (Proof.theory_of state)) src) state);
    1.22 +val invoke_case_i = ProofHistory.apply o Proof.invoke_case o Comment.ignore;
    1.23  
    1.24  
    1.25  (* statements *)