src/Pure/Isar/attrib.ML
changeset 28965 1de908189869
parent 28084 a05ca48ef263
child 29004 a5a91f387791
     1.1 --- a/src/Pure/Isar/attrib.ML	Wed Dec 03 21:00:39 2008 -0800
     1.2 +++ b/src/Pure/Isar/attrib.ML	Thu Dec 04 14:43:33 2008 +0100
     1.3 @@ -1,5 +1,4 @@
     1.4  (*  Title:      Pure/Isar/attrib.ML
     1.5 -    ID:         $Id$
     1.6      Author:     Markus Wenzel, TU Muenchen
     1.7  
     1.8  Symbolic representation of attributes -- with name and syntax.
     1.9 @@ -8,8 +7,8 @@
    1.10  signature ATTRIB =
    1.11  sig
    1.12    type src = Args.src
    1.13 -  type binding = Name.binding * src list
    1.14 -  val no_binding: binding
    1.15 +  type binding = Binding.T * src list
    1.16 +  val empty_binding: binding
    1.17    val print_attributes: theory -> unit
    1.18    val intern: theory -> xstring -> string
    1.19    val intern_src: theory -> src -> src
    1.20 @@ -55,8 +54,8 @@
    1.21  
    1.22  type src = Args.src;
    1.23  
    1.24 -type binding = Name.binding * src list;
    1.25 -val no_binding: binding = (Name.no_binding, []);
    1.26 +type binding = Binding.T * src list;
    1.27 +val empty_binding: binding = (Binding.empty, []);
    1.28  
    1.29  
    1.30  
    1.31 @@ -119,7 +118,7 @@
    1.32  fun attribute thy = attribute_i thy o intern_src thy;
    1.33  
    1.34  fun eval_thms ctxt args = ProofContext.note_thmss Thm.theoremK
    1.35 -    [((Name.no_binding, []),
    1.36 +    [((Binding.empty, []),
    1.37        map (apsnd (map (attribute (ProofContext.theory_of ctxt)))) args)] ctxt
    1.38    |> fst |> maps snd;
    1.39  
    1.40 @@ -373,7 +372,7 @@
    1.41  fun register_config config thy =
    1.42    let
    1.43      val bname = Config.name_of config;
    1.44 -    val name = Sign.full_name thy bname;
    1.45 +    val name = Sign.full_bname thy bname;
    1.46    in
    1.47      thy
    1.48      |> add_attributes [(bname, syntax (Scan.lift (scan_config thy config) >> Morphism.form),