# HG changeset patch
# User wenzelm
# Date 1526239228 -7200
# Node ID 7ed88a534bb6bd2be738100912df961310e841c0
# Parent  0f14cf9c632fe17563a7eb3f330951a8315c5c63
more uniform types vs. consts;

diff -r 0f14cf9c632f -r 7ed88a534bb6 src/Pure/Thy/export_theory.ML
--- a/src/Pure/Thy/export_theory.ML	Sun May 13 20:24:33 2018 +0200
+++ b/src/Pure/Thy/export_theory.ML	Sun May 13 21:20:28 2018 +0200
@@ -20,11 +20,11 @@
     val props = Markup.serial_properties serial @ Position.offset_properties_of pos;
   in (Markup.entityN, (Markup.nameN, name) :: props) end;
 
-fun export_decls export_decl parents space decls =
+fun export_decls export_decl parents thy space decls =
   (decls, []) |-> fold (fn (name, decl) =>
     if exists (fn space => Name_Space.declared space name) parents then I
     else
-      (case export_decl decl of
+      (case export_decl thy name decl of
         NONE => I
       | SOME body => cons (name, XML.Elem (entity_markup space name, body))))
   |> sort_by #1 |> map #2;
@@ -34,7 +34,7 @@
 
 fun present get_space get_decls export name thy =
   if Options.default_bool "export_theory" then
-    (case export (map get_space (Theory.parents_of thy)) (get_space thy) (get_decls thy) of
+    (case export (map get_space (Theory.parents_of thy)) thy (get_space thy) (get_decls thy) of
       [] => ()
     | body => Export.export thy ("theory/" ^ name) [YXML.string_of_body body])
   else ();
@@ -62,7 +62,7 @@
 
 in
 
-val _ = setup_presentation (present_types export_type "types");
+val _ = setup_presentation (present_types (K (K export_type)) "types");
 
 end;
 
@@ -76,11 +76,18 @@
 
 val encode_const =
   let open XML.Encode Term_XML.Encode
-  in pair typ (option term) end;
+  in triple (list string) typ (option term) end;
+
+fun export_const thy c (T, abbrev) =
+  let
+    val T' = T |> Logic.unvarifyT_global |> Type.strip_sorts;
+    val abbrev' = abbrev |> Option.map (Logic.unvarify_global #> map_types Type.strip_sorts);
+    val args = map (#1 o dest_TFree) (Consts.typargs (Sign.consts_of thy) (c, T'));
+  in SOME (encode_const (args, T', abbrev')) end;
 
 in
 
-val _ = setup_presentation (present_consts (SOME o encode_const) "consts");
+val _ = setup_presentation (present_consts export_const "consts");
 
 end;
 
diff -r 0f14cf9c632f -r 7ed88a534bb6 src/Pure/Thy/export_theory.scala
--- a/src/Pure/Thy/export_theory.scala	Sun May 13 20:24:33 2018 +0200
+++ b/src/Pure/Thy/export_theory.scala	Sun May 13 21:20:28 2018 +0200
@@ -34,9 +34,6 @@
   /* types */
 
   sealed case class Type(entity: Entity, args: List[String], abbrev: Option[Term.Typ])
-  {
-    def arity: Int = args.length
-  }
 
   def decode_type(tree: XML.Tree): Type =
   {
@@ -52,16 +49,17 @@
 
   /* consts */
 
-  sealed case class Const(entity: Entity, typ: Term.Typ, abbrev: Option[Term.Term])
+  sealed case class Const(
+    entity: Entity, typargs: List[String], typ: Term.Typ, abbrev: Option[Term.Term])
 
   def decode_const(tree: XML.Tree): Const =
   {
     val (entity, body) = decode_entity(tree)
-    val (typ, abbrev) =
+    val (args, typ, abbrev) =
     {
       import XML.Decode._
-      pair(Term_XML.Decode.typ, option(Term_XML.Decode.term))(body)
+      triple(list(string), Term_XML.Decode.typ, option(Term_XML.Decode.term))(body)
     }
-    Const(entity, typ, abbrev)
+    Const(entity, args, typ, abbrev)
   }
 }