invoke_case: include attributes;
authorwenzelm
Tue Mar 14 11:33:14 2000 +0100 (2000-03-14 ago)
changeset 8450dc44d6533f0f
parent 8449 f8ff23736465
child 8451 614f18139d47
invoke_case: include attributes;
src/Pure/Isar/isar_syn.ML
src/Pure/Isar/isar_thy.ML
src/Pure/Isar/proof.ML
     1.1 --- a/src/Pure/Isar/isar_syn.ML	Tue Mar 14 11:32:38 2000 +0100
     1.2 +++ b/src/Pure/Isar/isar_syn.ML	Tue Mar 14 11:33:14 2000 +0100
     1.3 @@ -345,7 +345,7 @@
     1.4  
     1.5  val caseP =
     1.6    OuterSyntax.command "case" "invoke local context" K.prf_asm
     1.7 -    (P.xname -- P.marg_comment >> (Toplevel.print oo (Toplevel.proof o IsarThy.invoke_case)));
     1.8 +    (P.xthm -- P.marg_comment >> (Toplevel.print oo (Toplevel.proof o IsarThy.invoke_case)));
     1.9  
    1.10  
    1.11  (* proof structure *)
     2.1 --- a/src/Pure/Isar/isar_thy.ML	Tue Mar 14 11:32:38 2000 +0100
     2.2 +++ b/src/Pure/Isar/isar_thy.ML	Tue Mar 14 11:33:14 2000 +0100
     2.3 @@ -79,7 +79,9 @@
     2.4    val fix_i: ((string list * typ option) * Comment.text) list -> ProofHistory.T -> ProofHistory.T
     2.5    val match_bind: ((string list * string) * Comment.text) list -> ProofHistory.T -> ProofHistory.T
     2.6    val match_bind_i: ((term list * term) * Comment.text) list -> ProofHistory.T -> ProofHistory.T
     2.7 -  val invoke_case: string * Comment.text -> ProofHistory.T -> ProofHistory.T
     2.8 +  val invoke_case: (string * Args.src list) * Comment.text -> ProofHistory.T -> ProofHistory.T
     2.9 +  val invoke_case_i: (string * Proof.context attribute list) * Comment.text
    2.10 +    -> ProofHistory.T -> ProofHistory.T
    2.11    val theorem: (bstring * Args.src list * (string * (string list * string list)))
    2.12      * Comment.text -> bool -> theory -> ProofHistory.T
    2.13    val theorem_i: (bstring * theory attribute list * (term * (term list * term list)))
    2.14 @@ -288,7 +290,10 @@
    2.15  val fix_i = ProofHistory.apply o Proof.fix_i o map Comment.ignore;
    2.16  val match_bind = ProofHistory.apply o Proof.match_bind o map Comment.ignore;
    2.17  val match_bind_i = ProofHistory.apply o Proof.match_bind_i o map Comment.ignore;
    2.18 -val invoke_case = ProofHistory.apply o Proof.invoke_case o Comment.ignore;
    2.19 +
    2.20 +fun invoke_case ((name, src), comment_ignore) = ProofHistory.apply (fn state =>
    2.21 +  Proof.invoke_case (name, map (Attrib.local_attribute (Proof.theory_of state)) src) state);
    2.22 +val invoke_case_i = ProofHistory.apply o Proof.invoke_case o Comment.ignore;
    2.23  
    2.24  
    2.25  (* statements *)
     3.1 --- a/src/Pure/Isar/proof.ML	Tue Mar 14 11:32:38 2000 +0100
     3.2 +++ b/src/Pure/Isar/proof.ML	Tue Mar 14 11:33:14 2000 +0100
     3.3 @@ -67,7 +67,7 @@
     3.4      -> state -> state
     3.5    val presume_i: (string * context attribute list * (term * (term list * term list)) list) list
     3.6      -> state -> state
     3.7 -  val invoke_case: string -> state -> state
     3.8 +  val invoke_case: string * context attribute list -> state -> state
     3.9    val theorem: bstring -> theory attribute list -> string * (string list * string list)
    3.10      -> theory -> state
    3.11    val theorem_i: bstring -> theory attribute list -> term * (term list * term list)
    3.12 @@ -561,11 +561,11 @@
    3.13  
    3.14  (* invoke_case *)
    3.15  
    3.16 -fun invoke_case name state =
    3.17 +fun invoke_case (name, atts) state =
    3.18    let val (vars, props) = get_case state name in
    3.19      state
    3.20      |> fix_i (map (fn (x, T) => ([x], Some T)) vars)
    3.21 -    |> assume_i [(name, [], map (fn t => (t, ([], []))) props)]
    3.22 +    |> assume_i [(name, atts, map (fn t => (t, ([], []))) props)]
    3.23    end;
    3.24  
    3.25