src/Pure/Isar/locale.ML

     Locale of string |
     Rename of expr * (string * mixfix option) option list |
     Merge of expr list
   val empty: expr
   datatype 'a element = Elem of 'a | Expr of expr
+  val map_elem: ('a -> 'b) -> 'a element -> 'b element
 
   val intern: theory -> xstring -> string
   val extern: theory -> string -> xstring
   val init: string -> theory -> Proof.context
 

   val global_asms_of: theory -> string ->
     ((string * Attrib.src list) * term list) list
 
   (* Processing of locale statements *)
   val read_context_statement: xstring option -> Element.context element list ->
+    (string * string list) list list -> Proof.context ->
+    string option * Proof.context * Proof.context * (term * term list) list list
+  val read_context_statement_i: string option -> Element.context element list ->
     (string * string list) list list -> Proof.context ->
     string option * Proof.context * Proof.context * (term * term list) list list
   val cert_context_statement: string option -> Element.context_i element list ->
     (term * term list) list list -> Proof.context ->
     string option * Proof.context * Proof.context * (term * term list) list list

 
     val prt_term = Pretty.quote o ProofContext.pretty_term ctxt;
     fun prt_inst ts =
         Pretty.enclose "(" ")" (Pretty.breaks (map prt_term ts));
     fun prt_attn (prfx, atts) =
-        Pretty.breaks (Pretty.str prfx :: Args.pretty_attribs ctxt atts);
+        Pretty.breaks (Pretty.str prfx :: Attrib.pretty_attribs ctxt atts);
     fun prt_witns witns = Pretty.enclose "[" "]"
       (Pretty.breaks (map (prt_term o Element.witness_prop) witns));
     fun prt_reg (ts, (("", []), witns)) =
         if show_wits
           then Pretty.block [prt_inst ts, Pretty.fbrk, prt_witns witns]

 fun cert_context import body ctxt = #1 (cert_ctxt true [] import (map Elem body) [] ctxt);
 
 val read_expr = prep_expr read_context;
 val cert_expr = prep_expr cert_context;
 
-fun read_context_statement raw_locale = prep_statement intern read_ctxt raw_locale ;
-fun cert_context_statement raw_locale = prep_statement (K I) cert_ctxt raw_locale ;
+fun read_context_statement loc = prep_statement intern read_ctxt loc;
+fun read_context_statement_i loc = prep_statement (K I) read_ctxt loc;
+fun cert_context_statement loc = prep_statement (K I) cert_ctxt loc;
 
 end;
 
 
 (* print locale *)