# HG changeset patch
# User wenzelm
# Date 1160861154 -7200
# Node ID 326c15917a33a80eb365559cbce34c86ed2026b0
# Parent  99697a1597b2d67a0fe3fbb2e60023d457edf38d
export map_elem;
added read_context_statement_i (internal locale name);

diff -r 99697a1597b2 -r 326c15917a33 src/Pure/Isar/locale.ML
--- a/src/Pure/Isar/locale.ML	Sat Oct 14 23:25:53 2006 +0200
+++ b/src/Pure/Isar/locale.ML	Sat Oct 14 23:25:54 2006 +0200
@@ -42,6 +42,7 @@
     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
@@ -62,6 +63,9 @@
   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
@@ -449,7 +453,7 @@
     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)) =
@@ -1440,8 +1444,9 @@
 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;