src/Pure/Isar/specification.ML
changeset 29581 b3b33e0298eb
parent 29249 4dc278c8dc59
child 29606 fedb8be05f24
     1.1 --- a/src/Pure/Isar/specification.ML	Wed Jan 21 16:47:31 2009 +0100
     1.2 +++ b/src/Pure/Isar/specification.ML	Wed Jan 21 16:47:32 2009 +0100
     1.3 @@ -9,33 +9,33 @@
     1.4  signature SPECIFICATION =
     1.5  sig
     1.6    val print_consts: local_theory -> (string * typ -> bool) -> (string * typ) list -> unit
     1.7 -  val check_specification: (Binding.T * typ option * mixfix) list ->
     1.8 +  val check_specification: (binding * typ option * mixfix) list ->
     1.9      (Attrib.binding * term list) list list -> Proof.context ->
    1.10 -    (((Binding.T * typ) * mixfix) list * (Attrib.binding * term list) list) * Proof.context
    1.11 -  val read_specification: (Binding.T * string option * mixfix) list ->
    1.12 +    (((binding * typ) * mixfix) list * (Attrib.binding * term list) list) * Proof.context
    1.13 +  val read_specification: (binding * string option * mixfix) list ->
    1.14      (Attrib.binding * string list) list list -> Proof.context ->
    1.15 -    (((Binding.T * typ) * mixfix) list * (Attrib.binding * term list) list) * Proof.context
    1.16 -  val check_free_specification: (Binding.T * typ option * mixfix) list ->
    1.17 +    (((binding * typ) * mixfix) list * (Attrib.binding * term list) list) * Proof.context
    1.18 +  val check_free_specification: (binding * typ option * mixfix) list ->
    1.19      (Attrib.binding * term list) list -> Proof.context ->
    1.20 -    (((Binding.T * typ) * mixfix) list * (Attrib.binding * term list) list) * Proof.context
    1.21 -  val read_free_specification: (Binding.T * string option * mixfix) list ->
    1.22 +    (((binding * typ) * mixfix) list * (Attrib.binding * term list) list) * Proof.context
    1.23 +  val read_free_specification: (binding * string option * mixfix) list ->
    1.24      (Attrib.binding * string list) list -> Proof.context ->
    1.25 -    (((Binding.T * typ) * mixfix) list * (Attrib.binding * term list) list) * Proof.context
    1.26 -  val axiomatization: (Binding.T * typ option * mixfix) list ->
    1.27 +    (((binding * typ) * mixfix) list * (Attrib.binding * term list) list) * Proof.context
    1.28 +  val axiomatization: (binding * typ option * mixfix) list ->
    1.29      (Attrib.binding * term list) list -> theory ->
    1.30      (term list * (string * thm list) list) * theory
    1.31 -  val axiomatization_cmd: (Binding.T * string option * mixfix) list ->
    1.32 +  val axiomatization_cmd: (binding * string option * mixfix) list ->
    1.33      (Attrib.binding * string list) list -> theory ->
    1.34      (term list * (string * thm list) list) * theory
    1.35    val definition:
    1.36 -    (Binding.T * typ option * mixfix) option * (Attrib.binding * term) ->
    1.37 +    (binding * typ option * mixfix) option * (Attrib.binding * term) ->
    1.38      local_theory -> (term * (string * thm)) * local_theory
    1.39    val definition_cmd:
    1.40 -    (Binding.T * string option * mixfix) option * (Attrib.binding * string) ->
    1.41 +    (binding * string option * mixfix) option * (Attrib.binding * string) ->
    1.42      local_theory -> (term * (string * thm)) * local_theory
    1.43 -  val abbreviation: Syntax.mode -> (Binding.T * typ option * mixfix) option * term ->
    1.44 +  val abbreviation: Syntax.mode -> (binding * typ option * mixfix) option * term ->
    1.45      local_theory -> local_theory
    1.46 -  val abbreviation_cmd: Syntax.mode -> (Binding.T * string option * mixfix) option * string ->
    1.47 +  val abbreviation_cmd: Syntax.mode -> (binding * string option * mixfix) option * string ->
    1.48      local_theory -> local_theory
    1.49    val notation: bool -> Syntax.mode -> (term * mixfix) list -> local_theory -> local_theory
    1.50    val notation_cmd: bool -> Syntax.mode -> (string * mixfix) list -> local_theory -> local_theory
    1.51 @@ -149,7 +149,8 @@
    1.52  
    1.53      (*axioms*)
    1.54      val (axioms, axioms_thy) = consts_thy |> fold_map (fn ((b, atts), props) =>
    1.55 -        fold_map Thm.add_axiom (PureThy.name_multi (Binding.base_name b) (map subst props))
    1.56 +        fold_map Thm.add_axiom
    1.57 +          ((map o apfst) Binding.name (PureThy.name_multi (Binding.base_name b) (map subst props)))
    1.58          #>> (fn ths => ((b, atts), [(map Drule.standard' ths, [])]))) specs;
    1.59      val (facts, thy') = axioms_thy |> PureThy.note_thmss Thm.axiomK
    1.60        (Attrib.map_facts (Attrib.attribute_i axioms_thy) axioms);