src/Pure/Isar/isar_thy.ML
changeset 18728 6790126ab5f6
parent 18678 dd0c569fa43d
child 18804 d42708f5c186
     1.1 --- a/src/Pure/Isar/isar_thy.ML	Fri Jan 20 04:53:59 2006 +0100
     1.2 +++ b/src/Pure/Isar/isar_thy.ML	Sat Jan 21 23:02:14 2006 +0100
     1.3 @@ -8,16 +8,16 @@
     1.4  signature ISAR_THY =
     1.5  sig
     1.6    val add_axioms: ((bstring * string) * Attrib.src list) list -> theory -> theory
     1.7 -  val add_axioms_i: ((bstring * term) * theory attribute list) list -> theory -> theory
     1.8 +  val add_axioms_i: ((bstring * term) * attribute list) list -> theory -> theory
     1.9    val add_defs: bool * ((bstring * string) * Attrib.src list) list -> theory -> theory
    1.10 -  val add_defs_i: bool * ((bstring * term) * theory attribute list) list -> theory -> theory
    1.11 +  val add_defs_i: bool * ((bstring * term) * attribute list) list -> theory -> theory
    1.12    val apply_theorems: (thmref * Attrib.src list) list -> theory -> thm list * theory
    1.13 -  val apply_theorems_i: (thm list * theory attribute list) list -> theory -> thm list * theory
    1.14 +  val apply_theorems_i: (thm list * attribute list) list -> theory -> thm list * theory
    1.15    val theorems: string ->
    1.16      ((bstring * Attrib.src list) * (thmref * Attrib.src list) list) list
    1.17      -> theory -> (string * thm list) list * theory 
    1.18    val theorems_i: string ->
    1.19 -    ((bstring * theory attribute list) * (thm list * theory attribute list) list) list
    1.20 +    ((bstring * attribute list) * (thm list * attribute list) list) list
    1.21      -> theory -> (string * thm list) list * theory
    1.22    val smart_theorems: string -> xstring option ->
    1.23      ((bstring * Attrib.src list) * (thmref * Attrib.src list) list) list ->
    1.24 @@ -34,7 +34,7 @@
    1.25      bool -> Proof.state -> Proof.state
    1.26    val theorem: string -> string * Attrib.src list -> string * (string list * string list) ->
    1.27      theory -> Proof.state
    1.28 -  val theorem_i: string -> string * theory attribute list -> term * (term list * term list) ->
    1.29 +  val theorem_i: string -> string * attribute list -> term * (term list * term list) ->
    1.30      theory -> Proof.state
    1.31    val qed: Method.text option -> Toplevel.transition -> Toplevel.transition
    1.32    val terminal_proof: Method.text * Method.text option ->
    1.33 @@ -58,7 +58,7 @@
    1.34  (* axioms and defs *)
    1.35  
    1.36  fun add_axms f args thy =
    1.37 -  f (map (fn (x, srcs) => (x, map (Attrib.global_attribute thy) srcs)) args) thy;
    1.38 +  f (map (fn (x, srcs) => (x, map (Attrib.attribute thy) srcs)) args) thy;
    1.39  
    1.40  val add_axioms = add_axms (snd oo PureThy.add_axioms);
    1.41  val add_axioms_i = snd oo PureThy.add_axioms_i;
    1.42 @@ -73,7 +73,7 @@
    1.43      Context.setmp (SOME thy) (Present.results (kind ^ "s")) named_thmss);
    1.44  
    1.45  fun theorems kind args thy = thy
    1.46 -  |> PureThy.note_thmss (Drule.kind kind) (Attrib.map_facts (Attrib.global_attribute thy) args)
    1.47 +  |> PureThy.note_thmss (Drule.kind kind) (Attrib.map_facts (Attrib.attribute thy) args)
    1.48    |> tap (present_theorems kind);
    1.49  
    1.50  fun theorems_i kind args =