# HG changeset patch
# User wenzelm
# Date 1575288189 -3600
# Node ID 7d522732b7f2c98a1434588f8bb124cffb154d9f
# Parent  66fa99c8509559610acace83f25060874d2b9496
more informative export;

diff -r 66fa99c85095 -r 7d522732b7f2 src/Pure/Thy/export_theory.ML
--- a/src/Pure/Thy/export_theory.ML	Mon Dec 02 12:03:55 2019 +0100
+++ b/src/Pure/Thy/export_theory.ML	Mon Dec 02 13:03:09 2019 +0100
@@ -122,7 +122,7 @@
 
 (* spec rules *)
 
-fun spec_content {pos, name, rough_classification, terms = terms0, rules = rules0} =
+fun spec_rule_content {pos, name, rough_classification, terms = terms0, rules = rules0} =
   let
     val terms = map Logic.unvarify_global terms0;
     val rules = map (Logic.unvarify_global o Thm.plain_prop_of) rules0;
@@ -133,7 +133,7 @@
     rough_classification = rough_classification,
     typargs = rev (fold Term.add_tfrees text []),
     args = rev (fold Term.add_frees text []),
-    terms = terms,
+    terms = map (fn t => (t, Term.type_of t)) terms,
     rules = rules}
   end;
 
@@ -425,14 +425,14 @@
         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))))))
+              (pair (list (pair encode_term typ)) (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" (encode_specs (map spec_content spec_rules)));
+      | spec_rules => export_body thy "spec_rules" (encode_specs (map spec_rule_content spec_rules)));
 
 
     (* parents *)
diff -r 66fa99c85095 -r 7d522732b7f2 src/Pure/Thy/export_theory.scala
--- a/src/Pure/Thy/export_theory.scala	Mon Dec 02 12:03:55 2019 +0100
+++ b/src/Pure/Thy/export_theory.scala	Mon Dec 02 13:03:09 2019 +0100
@@ -716,7 +716,7 @@
     rough_classification: Rough_Classification,
     typargs: List[(String, Term.Sort)],
     args: List[(String, Term.Typ)],
-    terms: List[Term.Term],
+    terms: List[(Term.Term, Term.Typ)],
     rules: List[Term.Term])
   {
     def id: Option[Long] = Position.Id.unapply(pos)
@@ -728,7 +728,7 @@
         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(_)),
+        terms.map({ case (term, typ) => (cache.term(term), cache.typ(typ)) }),
         rules.map(cache.term(_)))
   }
 
@@ -742,7 +742,7 @@
       list(
         pair(properties, pair(string, pair(decode_rough_classification,
           pair(list(pair(string, sort)), pair(list(pair(string, typ)),
-            pair(list(term), list(term))))))))(body)
+            pair(list(pair(term, typ)), list(term))))))))(body)
     }
     for ((pos, (name, (rough_classification, (typargs, (args, (terms, rules)))))) <- spec_rules)
       yield Spec_Rule(pos, name, rough_classification, typargs, args, terms, rules)