more exports;
read_session: proper signature;

--- a/src/HOL/Tools/typedef.ML	Thu May 24 09:18:29 2018 +0200
+++ b/src/HOL/Tools/typedef.ML	Thu May 24 16:56:14 2018 +0200
@@ -348,4 +348,27 @@
 
 val overloaded = typedef_overloaded;
 
+
+
+(** theory export **)
+
+val _ = Export_Theory.setup_presentation (fn _ => fn thy =>
+  let
+    val parent_spaces = map Sign.type_space (Theory.parents_of thy);
+    val typedefs =
+      Name_Space.dest_table (#types (Type.rep_tsig (Sign.tsig_of thy)))
+      |> maps (fn (name, _) =>
+          if exists (fn space => Name_Space.declared space name) parent_spaces then []
+          else
+            get_info_global thy name
+            |> map (fn ({rep_type, abs_type, Rep_name, Abs_name, axiom_name}, _) =>
+              (name, (rep_type, (abs_type, (Rep_name, (Abs_name, axiom_name)))))));
+  in
+    if null typedefs then ()
+    else
+      Export_Theory.export_body thy "typedefs"
+        let open XML.Encode Term_XML.Encode
+        in list (pair string (pair typ (pair typ (pair string (pair string string))))) typedefs end
+  end);
+
 end;

--- a/src/Pure/Thy/export_theory.ML	Thu May 24 09:18:29 2018 +0200
+++ b/src/Pure/Thy/export_theory.ML	Thu May 24 16:56:14 2018 +0200
@@ -27,6 +27,9 @@
 
 val _ = setup_presentation (fn {adjust_pos, ...} => fn thy =>
   let
+    val rep_tsig = Type.rep_tsig (Sign.tsig_of thy);
+
+
     (* parents *)
 
     val parents = Theory.parents_of thy;
@@ -76,7 +79,7 @@
 
     val _ =
       export_entities "types" (K export_type) Sign.type_space
-        (Name_Space.dest_table (#types (Type.rep_tsig (Sign.tsig_of thy))));
+        (Name_Space.dest_table (#types rep_tsig));
 
 
     (* consts *)
@@ -120,6 +123,24 @@
       export_entities "facts" (K (SOME o export_fact)) (Facts.space_of o Global_Theory.facts_of)
         (Facts.dest_static true [] (Global_Theory.facts_of thy));
 
+
+    (* type classes *)
+
+    val encode_class =
+      let open XML.Encode Term_XML.Encode
+      in pair (list (pair string typ)) (list term) end;
+
+    fun export_class name =
+      (case try (Axclass.get_info thy) name of
+        NONE => ([], [])
+      | SOME {params, axioms, ...} =>
+          (params, map (Logic.unvarify_global o Thm.full_prop_of) axioms))
+      |> encode_class |> SOME;
+
+    val _ =
+      export_entities "classes" (fn name => fn () => export_class name)
+        Sign.class_space (map (rpair ()) (Graph.keys (Sorts.classes_of (#2 (#classes rep_tsig)))));
+
     in () end);
 
 end;

--- a/src/Pure/Thy/export_theory.scala	Thu May 24 09:18:29 2018 +0200
+++ b/src/Pure/Thy/export_theory.scala	Thu May 24 16:56:14 2018 +0200
@@ -26,14 +26,19 @@
   def read_session(store: Sessions.Store,
     session_name: String,
     types: Boolean = true,
-    consts: Boolean = true): Session =
+    consts: Boolean = true,
+    axioms: Boolean = true,
+    facts: Boolean = true,
+    classes: Boolean = true,
+    typedefs: Boolean = true): Session =
   {
     val thys =
       using(store.open_database(session_name))(db =>
       {
         db.transaction {
           Export.read_theory_names(db, session_name).map((theory_name: String) =>
-            read_theory(db, session_name, theory_name, types = types, consts = consts))
+            read_theory(db, session_name, theory_name, types = types, consts = consts,
+              axioms = axioms, facts = facts, classes = classes, typedefs = typedefs))
         }
       })
 
@@ -55,18 +60,22 @@
     types: List[Type],
     consts: List[Const],
     axioms: List[Axiom],
-    facts: List[Fact])
+    facts: List[Fact],
+    classes: List[Class],
+    typedefs: List[Typedef])
   {
     override def toString: String = name
   }
 
-  def empty_theory(name: String): Theory = Theory(name, Nil, Nil, Nil, Nil, Nil)
+  def empty_theory(name: String): Theory = Theory(name, Nil, Nil, Nil, Nil, Nil, Nil, Nil)
 
   def read_theory(db: SQL.Database, session_name: String, theory_name: String,
     types: Boolean = true,
     consts: Boolean = true,
     axioms: Boolean = true,
-    facts: Boolean = true): Theory =
+    facts: Boolean = true,
+    classes: Boolean = true,
+    typedefs: Boolean = true): Theory =
   {
     val parents =
       Export.read_entry(db, session_name, theory_name, "theory/parents") match {
@@ -79,7 +88,9 @@
       if (types) read_types(db, session_name, theory_name) else Nil,
       if (consts) read_consts(db, session_name, theory_name) else Nil,
       if (axioms) read_axioms(db, session_name, theory_name) else Nil,
-      if (facts) read_facts(db, session_name, theory_name) else Nil)
+      if (facts) read_facts(db, session_name, theory_name) else Nil,
+      if (classes) read_classes(db, session_name, theory_name) else Nil,
+      if (typedefs) read_typedefs(db, session_name, theory_name) else Nil)
   }
 
 
@@ -104,13 +115,20 @@
     }
   }
 
+  def read_export[A](db: SQL.Database, session_name: String, theory_name: String,
+    export_name: String, decode: XML.Body => List[A]): List[A] =
+  {
+    Export.read_entry(db, session_name, theory_name, "theory/" + export_name) match {
+      case Some(entry) => decode(entry.uncompressed_yxml())
+      case None => Nil
+    }
+  }
+
   def read_entities[A](db: SQL.Database, session_name: String, theory_name: String,
     export_name: String, decode: XML.Tree => A): List[A] =
   {
-    Export.read_entry(db, session_name, theory_name, "theory/" + export_name) match {
-      case Some(entry) => entry.uncompressed_yxml().map(decode(_))
-      case None => Nil
-    }
+    read_export(db, session_name, theory_name, export_name,
+      (body: XML.Body) => body.map(decode(_)))
   }
 
 
@@ -190,4 +208,44 @@
           val (typargs, args, props) = decode_props(body)
           Fact(entity, typargs, args, props)
         })
+
+
+  /* type classes */
+
+  sealed case class Class(
+    entity: Entity, params: List[(String, Term.Typ)], axioms: List[Term.Term])
+
+  def read_classes(db: SQL.Database, session_name: String, theory_name: String): List[Class] =
+    read_entities(db, session_name, theory_name, "classes",
+      (tree: XML.Tree) =>
+        {
+          val (entity, body) = decode_entity(tree)
+          val (params, axioms) =
+          {
+            import XML.Decode._
+            import Term_XML.Decode._
+            pair(list(pair(string, typ)), list(term))(body)
+          }
+          Class(entity, params, axioms)
+        })
+
+
+  /* HOL typedefs */
+
+  sealed case class Typedef(name: String,
+    rep_type: Term.Typ, abs_type: Term.Typ, rep_name: String, abs_name: String, axiom_name: String)
+
+  def read_typedefs(db: SQL.Database, session_name: String, theory_name: String): List[Typedef] =
+    read_export(db, session_name, theory_name, "typedefs",
+      (body: XML.Body) =>
+        {
+          val typedefs =
+          {
+            import XML.Decode._
+            import Term_XML.Decode._
+            list(pair(string, pair(typ, pair(typ, pair(string, pair(string, string))))))(body)
+          }
+          for { (name, (rep_type, (abs_type, (rep_name, (abs_name, axiom_name))))) <- typedefs }
+          yield Typedef(name, rep_type, abs_type, rep_name, abs_name, axiom_name)
+        })
 }