# HG changeset patch
# User wenzelm
# Date 953029994 -3600
# Node ID dc44d6533f0f9992a64aff4502070b9cbe18711f
# Parent  f8ff237364659436c9fafef1fcc9525a39586d91
invoke_case: include attributes;

diff -r f8ff23736465 -r dc44d6533f0f src/Pure/Isar/isar_syn.ML
--- a/src/Pure/Isar/isar_syn.ML	Tue Mar 14 11:32:38 2000 +0100
+++ b/src/Pure/Isar/isar_syn.ML	Tue Mar 14 11:33:14 2000 +0100
@@ -345,7 +345,7 @@
 
 val caseP =
   OuterSyntax.command "case" "invoke local context" K.prf_asm
-    (P.xname -- P.marg_comment >> (Toplevel.print oo (Toplevel.proof o IsarThy.invoke_case)));
+    (P.xthm -- P.marg_comment >> (Toplevel.print oo (Toplevel.proof o IsarThy.invoke_case)));
 
 
 (* proof structure *)
diff -r f8ff23736465 -r dc44d6533f0f src/Pure/Isar/isar_thy.ML
--- a/src/Pure/Isar/isar_thy.ML	Tue Mar 14 11:32:38 2000 +0100
+++ b/src/Pure/Isar/isar_thy.ML	Tue Mar 14 11:33:14 2000 +0100
@@ -79,7 +79,9 @@
   val fix_i: ((string list * typ option) * Comment.text) list -> ProofHistory.T -> ProofHistory.T
   val match_bind: ((string list * string) * Comment.text) list -> ProofHistory.T -> ProofHistory.T
   val match_bind_i: ((term list * term) * Comment.text) list -> ProofHistory.T -> ProofHistory.T
-  val invoke_case: string * Comment.text -> ProofHistory.T -> ProofHistory.T
+  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)))
     * Comment.text -> bool -> theory -> ProofHistory.T
   val theorem_i: (bstring * theory attribute list * (term * (term list * term list)))
@@ -288,7 +290,10 @@
 val fix_i = ProofHistory.apply o Proof.fix_i o map Comment.ignore;
 val match_bind = ProofHistory.apply o Proof.match_bind o map Comment.ignore;
 val match_bind_i = ProofHistory.apply o Proof.match_bind_i o map Comment.ignore;
-val invoke_case = ProofHistory.apply o Proof.invoke_case o Comment.ignore;
+
+fun invoke_case ((name, src), comment_ignore) = ProofHistory.apply (fn state =>
+  Proof.invoke_case (name, map (Attrib.local_attribute (Proof.theory_of state)) src) state);
+val invoke_case_i = ProofHistory.apply o Proof.invoke_case o Comment.ignore;
 
 
 (* statements *)
diff -r f8ff23736465 -r dc44d6533f0f src/Pure/Isar/proof.ML
--- a/src/Pure/Isar/proof.ML	Tue Mar 14 11:32:38 2000 +0100
+++ b/src/Pure/Isar/proof.ML	Tue Mar 14 11:33:14 2000 +0100
@@ -67,7 +67,7 @@
     -> state -> state
   val presume_i: (string * context attribute list * (term * (term list * term list)) list) list
     -> state -> state
-  val invoke_case: string -> state -> state
+  val invoke_case: string * context attribute list -> state -> state
   val theorem: bstring -> theory attribute list -> string * (string list * string list)
     -> theory -> state
   val theorem_i: bstring -> theory attribute list -> term * (term list * term list)
@@ -561,11 +561,11 @@
 
 (* invoke_case *)
 
-fun invoke_case name state =
+fun invoke_case (name, atts) state =
   let val (vars, props) = get_case state name in
     state
     |> fix_i (map (fn (x, T) => ([x], Some T)) vars)
-    |> assume_i [(name, [], map (fn t => (t, ([], []))) props)]
+    |> assume_i [(name, atts, map (fn t => (t, ([], []))) props)]
   end;