src/Pure/Isar/locale.ML
changeset 28084 a05ca48ef263
parent 28083 103d9282a946
child 28085 914183e229e9
     1.1 --- a/src/Pure/Isar/locale.ML	Tue Sep 02 14:10:45 2008 +0200
     1.2 +++ b/src/Pure/Isar/locale.ML	Tue Sep 02 16:55:33 2008 +0200
     1.3 @@ -50,21 +50,16 @@
     1.4    val init: string -> theory -> Proof.context
     1.5  
     1.6    (* The specification of a locale *)
     1.7 -  val parameters_of: theory -> string ->
     1.8 -    ((string * typ) * mixfix) list
     1.9 -  val parameters_of_expr: theory -> expr ->
    1.10 -    ((string * typ) * mixfix) list
    1.11 -  val local_asms_of: theory -> string ->
    1.12 -    ((Name.binding * Attrib.src list) * term list) list
    1.13 -  val global_asms_of: theory -> string ->
    1.14 -    ((Name.binding * Attrib.src list) * term list) list
    1.15 +  val parameters_of: theory -> string -> ((string * typ) * mixfix) list
    1.16 +  val parameters_of_expr: theory -> expr -> ((string * typ) * mixfix) list
    1.17 +  val local_asms_of: theory -> string -> (Attrib.binding * term list) list
    1.18 +  val global_asms_of: theory -> string -> (Attrib.binding * term list) list
    1.19  
    1.20    (* Theorems *)
    1.21    val intros: theory -> string -> thm list * thm list
    1.22    val dests: theory -> string -> thm list
    1.23    (* Not part of the official interface.  DO NOT USE *)
    1.24 -  val facts_of: theory -> string
    1.25 -    -> ((Name.binding * Attrib.src list) * (thm list * Attrib.src list) list) list list
    1.26 +  val facts_of: theory -> string -> (Attrib.binding * (thm list * Attrib.src list) list) list list
    1.27  
    1.28    (* Processing of locale statements *)
    1.29    val read_context_statement: xstring option -> Element.context element list ->
    1.30 @@ -95,8 +90,7 @@
    1.31    val intro_locales_tac: bool -> Proof.context -> thm list -> tactic
    1.32  
    1.33    (* Storing results *)
    1.34 -  val add_thmss: string -> string ->
    1.35 -    ((Name.binding * Attrib.src list) * (thm list * Attrib.src list) list) list ->
    1.36 +  val add_thmss: string -> string -> (Attrib.binding * (thm list * Attrib.src list) list) list ->
    1.37      Proof.context -> Proof.context
    1.38    val add_type_syntax: string -> declaration -> Proof.context -> Proof.context
    1.39    val add_term_syntax: string -> declaration -> Proof.context -> Proof.context
    1.40 @@ -104,21 +98,21 @@
    1.41  
    1.42    val interpretation_i: (Proof.context -> Proof.context) ->
    1.43      (bool * string) * Attrib.src list -> expr ->
    1.44 -    term option list * ((Name.binding * Attrib.src list) * term) list ->
    1.45 +    term option list * (Attrib.binding * term) list ->
    1.46      theory -> Proof.state
    1.47    val interpretation: (Proof.context -> Proof.context) ->
    1.48      (bool * string) * Attrib.src list -> expr ->
    1.49 -    string option list * ((Name.binding * Attrib.src list) * string) list ->
    1.50 +    string option list * (Attrib.binding * string) list ->
    1.51      theory -> Proof.state
    1.52    val interpretation_in_locale: (Proof.context -> Proof.context) ->
    1.53      xstring * expr -> theory -> Proof.state
    1.54    val interpret_i: (Proof.state -> Proof.state Seq.seq) ->
    1.55      (bool * string) * Attrib.src list -> expr ->
    1.56 -    term option list * ((Name.binding * Attrib.src list) * term) list ->
    1.57 +    term option list * (Attrib.binding * term) list ->
    1.58      bool -> Proof.state -> Proof.state
    1.59    val interpret: (Proof.state -> Proof.state Seq.seq) ->
    1.60      (bool * string) * Attrib.src list -> expr ->
    1.61 -    string option list * ((Name.binding * Attrib.src list) * string) list ->
    1.62 +    string option list * (Attrib.binding * string) list ->
    1.63      bool -> Proof.state -> Proof.state
    1.64  end;
    1.65  
    1.66 @@ -1275,8 +1269,7 @@
    1.67      list_ord (fn ((_, (d1, _)), (_, (d2, _))) =>
    1.68        Term.fast_term_ord (d1, d2)) (defs1, defs2);
    1.69  structure Defstab =
    1.70 -    TableFun(type key = ((Name.binding * Attrib.src list) * (term * term list)) list
    1.71 -        val ord = defs_ord);
    1.72 +    TableFun(type key = (Attrib.binding * (term * term list)) list val ord = defs_ord);
    1.73  
    1.74  fun rem_dup_defs es ds =
    1.75      fold_map (fn e as (Defines defs) => (fn ds =>
    1.76 @@ -1908,7 +1901,7 @@
    1.77  
    1.78  fun defines_to_notes is_ext thy (Defines defs) defns =
    1.79      let
    1.80 -      val defs' = map (fn (_, (def, _)) => ((Name.no_binding, []), (def, []))) defs
    1.81 +      val defs' = map (fn (_, (def, _)) => (Attrib.no_binding, (def, []))) defs
    1.82        val notes = map (fn (a, (def, _)) =>
    1.83          (a, [([assume (cterm_of thy def)], [])])) defs
    1.84      in