# HG changeset patch
# User wenzelm
# Date 1533241456 -7200
# Node ID fc51dcb4e6fd8b0a8b7123d91e6a5cf679b620c8
# Parent  d1d03b7b6696b0e5f68cda10e723dc2379826e82
tuned signature: more operations;

diff -r d1d03b7b6696 -r fc51dcb4e6fd src/Pure/Thy/export_theory.scala
--- a/src/Pure/Thy/export_theory.scala	Thu Aug 02 21:49:31 2018 +0200
+++ b/src/Pure/Thy/export_theory.scala	Thu Aug 02 22:24:16 2018 +0200
@@ -174,6 +174,8 @@
 
   sealed case class Type(entity: Entity, args: List[String], abbrev: Option[Term.Typ])
   {
+    def kind: String = "type"
+
     def cache(cache: Term.Cache): Type =
       Type(entity.cache(cache),
         args.map(cache.string(_)),
@@ -198,6 +200,8 @@
   sealed case class Const(
     entity: Entity, typargs: List[String], typ: Term.Typ, abbrev: Option[Term.Term])
   {
+    def kind: String = "const"
+
     def cache(cache: Term.Cache): Const =
       Const(entity.cache(cache),
         typargs.map(cache.string(_)),
@@ -234,6 +238,8 @@
     args: List[(String, Term.Typ)],
     prop: Term.Term)
   {
+    def kind: String = "axiom"
+
     def cache(cache: Term.Cache): Axiom =
       Axiom(entity.cache(cache),
         typargs.map({ case (name, sort) => (cache.string(name), cache.sort(sort)) }),
@@ -255,6 +261,8 @@
     args: List[(String, Term.Typ)],
     props: List[Term.Term])
   {
+    def kind: String = "fact"
+
     def cache(cache: Term.Cache): Fact =
       Fact(entity.cache(cache),
         typargs.map({ case (name, sort) => (cache.string(name), cache.sort(sort)) }),
@@ -276,6 +284,8 @@
   sealed case class Class(
     entity: Entity, params: List[(String, Term.Typ)], axioms: List[Term.Term])
   {
+    def kind: String = "class"
+
     def cache(cache: Term.Cache): Class =
       Class(entity.cache(cache),
         params.map({ case (name, typ) => (cache.string(name), cache.typ(typ)) }),