# HG changeset patch
# User wenzelm
# Date 1537388316 -7200
# Node ID a6ba77af64862a030e526a7b1681b377abd53ca1
# Parent  7d77eab54b178ceb39066a92cd3bb253c609889c
export semi-unfolded locale axioms;

diff -r 7d77eab54b17 -r a6ba77af6486 src/Pure/Thy/export_theory.ML
--- a/src/Pure/Thy/export_theory.ML	Wed Sep 19 21:06:12 2018 +0200
+++ b/src/Pure/Thy/export_theory.ML	Wed Sep 19 22:18:36 2018 +0200
@@ -35,6 +35,25 @@
 end;
 
 
+(* locale support *)
+
+fun locale_axioms thy loc =
+  let
+    val (intro1, intro2) = Locale.intros_of thy loc;
+    fun intros_tac ctxt = Method.try_intros_tac ctxt (the_list intro1 @ the_list intro2);
+    val res =
+      Proof_Context.init_global thy
+      |> Interpretation.interpretation ([(loc, (("", false), (Expression.Named [], [])))], [])
+      |> Proof.refine (Method.Basic (METHOD o intros_tac))
+      |> Seq.filter_results
+      |> try Seq.hd;
+  in
+    (case res of
+      SOME st => Thm.prems_of (#goal (Proof.goal st))
+    | NONE => raise Fail ("Cannot unfold locale " ^ quote loc))
+  end;
+
+
 (* general setup *)
 
 fun setup_presentation f =
@@ -212,20 +231,18 @@
 
     (* locales *)
 
-    fun encode_locale ({type_params, params, asm, defs}: Locale.content) =
+    fun encode_locale loc ({type_params, params, ...}: Locale.content) =
       let
+        val axioms = locale_axioms thy loc;
         val args = map #1 params;
-        val typargs = type_params @ rev (fold Term.add_tfrees (map Free args @ the_list asm) []);
+        val typargs = type_params @ rev (fold Term.add_tfrees (map Free args @ axioms) []);
         val encode =
-          let open XML.Encode Term_XML.Encode in
-            pair (list (pair string sort))
-              (pair (list (pair string typ))
-                (pair (option term) (list term)))
-          end;
-      in encode (typargs, (args, (asm, defs))) end;
+          let open XML.Encode Term_XML.Encode
+          in triple (list (pair string sort)) (list (pair string typ)) (list term) end;
+      in encode (typargs, args, axioms) end;
 
     val _ =
-      export_entities "locales" (fn _ => SOME o encode_locale) Locale.locale_space
+      export_entities "locales" (SOME oo encode_locale) Locale.locale_space
         (Locale.dest_locales thy);
 
 
diff -r 7d77eab54b17 -r a6ba77af6486 src/Pure/Thy/export_theory.scala
--- a/src/Pure/Thy/export_theory.scala	Wed Sep 19 21:06:12 2018 +0200
+++ b/src/Pure/Thy/export_theory.scala	Wed Sep 19 22:18:36 2018 +0200
@@ -353,30 +353,29 @@
   /* locales */
 
   sealed case class Locale(
-    entity: Entity, typargs: List[(String, Term.Sort)], args: List[(String, Term.Typ)],
-      asm: Option[Term.Term], defs: List[Term.Term])
+    entity: Entity,
+    typargs: List[(String, Term.Sort)],
+    args: List[(String, Term.Typ)],
+    axioms: List[Term.Term])
   {
     def cache(cache: Term.Cache): Locale =
       Locale(entity.cache(cache),
         typargs.map({ case (name, sort) => (cache.string(name), cache.sort(sort)) }),
         args.map({ case (name, typ) => (cache.string(name), cache.typ(typ)) }),
-        asm.map(cache.term(_)),
-        defs.map(cache.term(_)))
+        axioms.map(cache.term(_)))
   }
 
   def read_locales(provider: Export.Provider): List[Locale] =
     provider.uncompressed_yxml(export_prefix + "locales").map((tree: XML.Tree) =>
       {
         val (entity, body) = decode_entity(Kind.LOCALE, tree)
-        val (typargs, (args, (asm, defs))) =
+        val (typargs, args, axioms) =
         {
           import XML.Decode._
           import Term_XML.Decode._
-          pair(list(pair(string, sort)),
-            pair(list(pair(string, typ)),
-              pair(option(term), list(term))))(body)
+          triple(list(pair(string, sort)), list(pair(string, typ)), list(term))(body)
         }
-        Locale(entity, typargs, args, asm, defs)
+        Locale(entity, typargs, args, axioms)
       })