# HG changeset patch
# User wenzelm
# Date 1138894295 -3600
# Node ID f984f22f1cb4a2e034b9a4247c5fb75dc6193e39
# Parent  2487aea6ff12fc2bb02094d2477a067650161b31
Proof.refine_insert;
statements: always use Attrib.src;

diff -r 2487aea6ff12 -r f984f22f1cb4 src/Pure/Isar/locale.ML
--- a/src/Pure/Isar/locale.ML	Thu Feb 02 16:31:34 2006 +0100
+++ b/src/Pure/Isar/locale.ML	Thu Feb 02 16:31:35 2006 +0100
@@ -95,7 +95,7 @@
     string * Attrib.src list -> Element.context element list -> Element.statement ->
     theory -> Proof.state
   val theorem_i: string -> Method.text option -> (thm list list -> theory -> theory) ->
-    string * attribute list -> Element.context_i element list -> Element.statement_i ->
+    string * Attrib.src list -> Element.context_i element list -> Element.statement_i ->
     theory -> Proof.state
   val theorem_in_locale: string -> Method.text option ->
     (thm list list -> thm list list -> theory -> theory) ->
@@ -104,7 +104,7 @@
   val theorem_in_locale_i: string -> Method.text option ->
     (thm list list -> thm list list -> theory -> theory) ->
     string -> string * Attrib.src list -> Element.context_i element list ->
-    (typ, term, Attrib.src) Element.stmt -> theory -> Proof.state
+    Element.statement_i -> theory -> Proof.state
   val smart_theorem: string -> xstring option ->
     string * Attrib.src list -> Element.context element list -> Element.statement ->
     theory -> Proof.state
@@ -118,7 +118,6 @@
 structure Locale: LOCALE =
 struct
 
-
 (** locale elements and expressions **)
 
 datatype ctxt = datatype Element.ctxt;
@@ -1736,18 +1735,18 @@
 fun intern_attrib thy = map_elem (Element.map_ctxt
   {name = I, var = I, typ = I, term = I, fact = I, attrib = Attrib.intern_src thy});
 
-fun global_goal prep_att =
-  Proof.global_goal ProofDisplay.present_results prep_att ProofContext.bind_propp_schematic_i;
-
-fun insert_facts [] = I
-  | insert_facts ths = Seq.hd o Proof.refine (Method.Basic (K (Method.insert ths)));
+val global_goal = Proof.global_goal ProofDisplay.present_results
+  Attrib.attribute_i ProofContext.bind_propp_schematic_i;
 
-fun conclusion (Element.Shows concl) = (([], concl), fn stmt => fn ctxt => ((stmt, []), ctxt))
-  | conclusion (Element.Obtains cases) = apfst (apfst (map Elem)) (Obtain.statement cases);
+fun conclusion prep_att (Element.Shows concl) =
+      (([], concl), fn stmt => fn ctxt => ((Attrib.map_specs prep_att stmt, []), ctxt))
+  | conclusion _ (Element.Obtains cases) = apfst (apfst (map Elem)) (Obtain.statement cases);
 
-fun gen_theorem prep_att prep_elem prep_stmt kind before_qed after_qed a raw_elems raw_concl thy =
+fun gen_theorem prep_src prep_elem prep_stmt
+    kind before_qed after_qed (name, raw_atts) raw_elems raw_concl thy =
   let
-    val ((concl_elems, concl), mk_stmt) = conclusion raw_concl;
+    val atts = map (prep_src thy) raw_atts;
+    val ((concl_elems, concl), mk_stmt) = conclusion (prep_src thy) raw_concl;
     val thy_ctxt = ProofContext.init thy;
     val elems = map (prep_elem thy) (raw_elems @ concl_elems);
     val (_, _, (view, ctxt), propp) = prep_stmt NONE elems (map snd concl) thy_ctxt;
@@ -1755,14 +1754,14 @@
       |> ProofContext.add_view thy_ctxt view
       |> mk_stmt (map fst concl ~~ propp);
   in
-    global_goal prep_att kind before_qed after_qed (SOME "") a stmt goal_ctxt
-    |> insert_facts facts
+    global_goal kind before_qed after_qed (SOME "") (name, atts) stmt goal_ctxt
+    |> Proof.refine_insert facts
   end;
 
 fun gen_theorem_in_locale prep_locale prep_src prep_elem prep_stmt no_target
     kind before_qed after_qed raw_loc (name, atts) raw_elems raw_concl thy =
   let
-    val ((concl_elems, concl), mk_stmt) = conclusion raw_concl;
+    val ((concl_elems, concl), mk_stmt) = conclusion (prep_src thy) raw_concl;
     val loc = prep_locale thy raw_loc;
     val loc_atts = map (prep_src thy) atts;
     val loc_attss = map (map (prep_src thy) o snd o fst) concl;
@@ -1793,13 +1792,13 @@
         #> after_qed loc_results results
       end;
   in
-    global_goal (K I) kind before_qed after_qed' target (name, []) stmt goal_ctxt
-    |> insert_facts facts
+    global_goal kind before_qed after_qed' target (name, []) stmt goal_ctxt
+    |> Proof.refine_insert facts
   end;
 
 in
 
-val theorem = gen_theorem Attrib.attribute intern_attrib read_context_statement;
+val theorem = gen_theorem Attrib.intern_src intern_attrib read_context_statement;
 val theorem_i = gen_theorem (K I) (K I) cert_context_statement;
 
 val theorem_in_locale = gen_theorem_in_locale intern Attrib.intern_src intern_attrib
diff -r 2487aea6ff12 -r f984f22f1cb4 src/Pure/Isar/obtain.ML
--- a/src/Pure/Isar/obtain.ML	Thu Feb 02 16:31:34 2006 +0100
+++ b/src/Pure/Isar/obtain.ML	Thu Feb 02 16:31:35 2006 +0100
@@ -49,9 +49,9 @@
   val guess_i: (string * typ option) list -> bool -> Proof.state -> Proof.state
   val statement: (string * ((string * 'typ option) list * 'term list)) list ->
     (('typ, 'term, 'fact) Element.ctxt list *
-      ((string * 'a list) * ('term * ('term list * 'term list)) list) list) *
-    (((string * 'b list) * (term * (term list * term list)) list) list -> Proof.context ->
-      (((string * 'c list) * (term * (term list * term list)) list) list * thm list) *
+      ((string * Attrib.src list) * ('term * ('term list * 'term list)) list) list) *
+    (((string * Attrib.src list) * (term * (term list * term list)) list) list -> Proof.context ->
+      (((string * Attrib.src list) * (term * (term list * term list)) list) list * thm list) *
         Proof.context)
 end;
 
@@ -158,7 +158,7 @@
     |> `Proof.the_facts
     ||> Proof.chain_facts chain_facts
     ||> Proof.show_i NONE after_qed [(("", []), [(thesis, ([], []))])] false
-    |-> (Proof.refine o Method.Basic o K o Method.insert) |> Seq.hd
+    |-> Proof.refine_insert
   end;
 
 in
@@ -281,6 +281,8 @@
 
 fun statement cases =
   let
+    val names =
+      cases |> map_index (fn (i, ("", _)) => string_of_int (i + 1) | (_, (name, _)) => name);
     val elems = cases |> map (fn (_, (vars, _)) =>
       Element.Constrains (vars |> List.mapPartial (fn (x, SOME T) => SOME (x, T) | _ => NONE)));
     val concl = cases |> map (fn (_, (_, props)) => (("", []), map (rpair ([], [])) props));
@@ -289,6 +291,9 @@
       let
         val thesis =
           ObjectLogic.fixed_judgment (ProofContext.theory_of ctxt) AutoBind.thesisN;
+        val atts = map Attrib.internal
+          [RuleCases.consumes (~ (length cases)), RuleCases.case_names names];
+
         fun assume_case ((name, (vars, _)), (_, propp)) ctxt' =
           let
             val xs = map fst vars;
@@ -308,7 +313,7 @@
           |> (snd o ProofContext.add_fixes_i [(AutoBind.thesisN, NONE, NoSyn)])
           |> fold_map assume_case (cases ~~ stmt)
           |-> (fn ths => ProofContext.note_thmss_i [((thatN, []), [(ths, [])])] #> #2 #> pair ths);
-      in (([(("", []), [(thesis, ([], []))])], ths), ctxt') end;
+      in (([(("", atts), [(thesis, ([], []))])], ths), ctxt') end;
   in ((elems, concl), mk_stmt) end;
 
 end;