src/Pure/Isar/attrib.ML
changeset 33095 bbd52d2f8696
parent 33092 c859019d3ac5
child 33096 db3c18fd9708
     1.1 --- a/src/Pure/Isar/attrib.ML	Sat Oct 24 19:24:50 2009 +0200
     1.2 +++ b/src/Pure/Isar/attrib.ML	Sat Oct 24 19:47:37 2009 +0200
     1.3 @@ -67,11 +67,11 @@
     1.4  
     1.5  structure Attributes = TheoryDataFun
     1.6  (
     1.7 -  type T = ((src -> attribute) * string) NameSpace.table;
     1.8 -  val empty = NameSpace.empty_table;
     1.9 +  type T = ((src -> attribute) * string) Name_Space.table;
    1.10 +  val empty = Name_Space.empty_table;
    1.11    val copy = I;
    1.12    val extend = I;
    1.13 -  fun merge _ tables : T = NameSpace.merge_tables tables;
    1.14 +  fun merge _ tables : T = Name_Space.merge_tables tables;
    1.15  );
    1.16  
    1.17  fun print_attributes thy =
    1.18 @@ -80,20 +80,20 @@
    1.19      fun prt_attr (name, (_, comment)) = Pretty.block
    1.20        [Pretty.str (name ^ ":"), Pretty.brk 2, Pretty.str comment];
    1.21    in
    1.22 -    [Pretty.big_list "attributes:" (map prt_attr (NameSpace.extern_table attribs))]
    1.23 +    [Pretty.big_list "attributes:" (map prt_attr (Name_Space.extern_table attribs))]
    1.24      |> Pretty.chunks |> Pretty.writeln
    1.25    end;
    1.26  
    1.27  fun add_attribute name att comment thy = thy
    1.28 -  |> Attributes.map (#2 o NameSpace.define true (Sign.naming_of thy) (name, (att, comment)));
    1.29 +  |> Attributes.map (#2 o Name_Space.define true (Sign.naming_of thy) (name, (att, comment)));
    1.30  
    1.31  
    1.32  (* name space *)
    1.33  
    1.34 -val intern = NameSpace.intern o #1 o Attributes.get;
    1.35 +val intern = Name_Space.intern o #1 o Attributes.get;
    1.36  val intern_src = Args.map_name o intern;
    1.37  
    1.38 -val extern = NameSpace.extern o #1 o Attributes.get o ProofContext.theory_of;
    1.39 +val extern = Name_Space.extern o #1 o Attributes.get o ProofContext.theory_of;
    1.40  
    1.41  
    1.42  (* pretty printing *)
    1.43 @@ -338,7 +338,7 @@
    1.44          Pretty.block [Pretty.str (name ^ ": " ^ Config.print_type value ^ " ="), Pretty.brk 1,
    1.45            Pretty.str (Config.print_value value)]
    1.46        end;
    1.47 -    val configs = NameSpace.extern_table (#1 (Attributes.get thy), Configs.get thy);
    1.48 +    val configs = Name_Space.extern_table (#1 (Attributes.get thy), Configs.get thy);
    1.49    in Pretty.writeln (Pretty.big_list "configuration options" (map prt configs)) end;
    1.50  
    1.51