clarified export of spec rules: more like locale;

--- a/src/Pure/Thy/export_theory.ML	Sun Dec 01 21:29:08 2019 +0100
+++ b/src/Pure/Thy/export_theory.ML	Mon Dec 02 11:57:42 2019 +0100
@@ -120,6 +120,25 @@
       in SOME (dep, (substT, subst)) end);
 
 
+(* spec rules *)
+
+fun spec_content (spec: Spec_Rules.spec) =
+  let
+    val {pos, name, rough_classification, terms = terms0, rules = rules0} = spec;
+    val terms = map Logic.unvarify_global terms0;
+    val rules = map (Logic.unvarify_global o Thm.plain_prop_of) rules0;
+    val text = terms @ rules;
+  in
+   {props = Position.properties_of pos,
+    name = name,
+    rough_classification = rough_classification,
+    typargs = rev (fold Term.add_tfrees text []),
+    args = rev (fold Term.add_frees text []),
+    terms = terms,
+    rules = rules}
+  end;
+
+
 (* general setup *)
 
 fun setup_presentation f =
@@ -402,21 +421,19 @@
 
     (* spec rules *)
 
-    fun encode_spec {pos, name, rough_classification, terms, rules} =
-      let
-        val terms' = map Logic.unvarify_global terms;
-        val rules' = map (fn rule => #1 (standard_prop_of (prep_thm rule) NONE)) rules;
-        open XML.Encode;
-      in
-        pair properties (pair string (pair Spec_Rules.encode_rough_classification
-          (pair (list encode_term) (list encode_prop))))
-          (Position.properties_of pos, (name, (rough_classification, (terms', rules'))))
+    val encode_specs =
+      let open XML.Encode Term_XML.Encode in
+        list (fn {props, name, rough_classification, typargs, args, terms, rules} =>
+          pair properties (pair string (pair Spec_Rules.encode_rough_classification
+            (pair (list (pair string sort)) (pair (list (pair string typ))
+              (pair (list encode_term) (list encode_term))))))
+              (props, (name, (rough_classification, (typargs, (args, (terms, rules)))))))
       end;
 
     val _ =
       (case Spec_Rules.dest_theory thy of
         [] => ()
-      | spec_rules => export_body thy "spec_rules" (XML.Encode.list encode_spec spec_rules));
+      | spec_rules => export_body thy "spec_rules" (encode_specs (map spec_content spec_rules)));
 
 
     (* parents *)

--- a/src/Pure/Thy/export_theory.scala	Sun Dec 01 21:29:08 2019 +0100
+++ b/src/Pure/Thy/export_theory.scala	Mon Dec 02 11:57:42 2019 +0100
@@ -714,8 +714,10 @@
     pos: Position.T,
     name: String,
     rough_classification: Rough_Classification,
+    typargs: List[(String, Term.Sort)],
+    args: List[(String, Term.Typ)],
     terms: List[Term.Term],
-    rules: List[Prop])
+    rules: List[Term.Term])
   {
     def id: Option[Long] = Position.Id.unapply(pos)
 
@@ -724,8 +726,10 @@
         cache.position(pos),
         cache.string(name),
         rough_classification.cache(cache),
+        typargs.map({ case (name, sort) => (cache.string(name), cache.sort(sort)) }),
+        args.map({ case (name, typ) => (cache.string(name), cache.typ(typ)) }),
         terms.map(cache.term(_)),
-        rules.map(_.cache(cache)))
+        rules.map(cache.term(_)))
   }
 
   def read_spec_rules(provider: Export.Provider): List[Spec_Rule] =
@@ -737,9 +741,10 @@
       import Term_XML.Decode._
       list(
         pair(properties, pair(string, pair(decode_rough_classification,
-        pair(list(term), list(decode_prop))))))(body)
+          pair(list(pair(string, sort)), pair(list(pair(string, typ)),
+            pair(list(term), list(term))))))))(body)
     }
-    for ((pos, (name, (rough_classification, (terms, rules)))) <- spec_rules)
-      yield Spec_Rule(pos, name, rough_classification, terms, rules)
+    for ((pos, (name, (rough_classification, (typargs, (args, (terms, rules)))))) <- spec_rules)
+      yield Spec_Rule(pos, name, rough_classification, typargs, args, terms, rules)
   }
 }