src/Pure/Thy/export_theory.ML

         val typargs = rev (add_tfrees used prop []);
         val used_typargs = fold (Name.declare o #1) typargs used;
         val sorts = Name.invent used_typargs Name.aT (length extra_shyps) ~~ extra_shyps;
       in ((sorts @ typargs, args, prop), proof) end;
 
+    fun standard_prop_of thm =
+      standard_prop Name.context (Thm.extra_shyps thm) (Thm.full_prop_of thm);
+
     val encode_prop =
       let open XML.Encode Term_XML.Encode
       in triple (list (pair string sort)) (list (pair string typ)) encode_term end;
 
     fun encode_axiom used prop =

 
 
     (* theorems and proof terms *)
 
     val clean_thm = Thm.check_hyps (Context.Theory thy) #> Thm.strip_shyps;
+    val prep_thm = clean_thm #> Thm.unconstrainT;
 
     val lookup_thm_id = Global_Theory.lookup_thm_id thy;
 
     fun expand_name thm_id (header: Proofterm.thm_header) =
       if #serial header = #serial thm_id then ""

       in make_entity_markup (Thm_Name.print (name, i)) (Thm_Name.print (xname, i)) pos serial end;
 
     fun encode_thm thm_id raw_thm =
       let
         val deps = map (Thm_Name.print o #2) (Thm_Deps.thm_deps thy [raw_thm]);
-        val thm = clean_thm (Thm.unconstrainT raw_thm);
+        val thm = prep_thm raw_thm;
 
         val proof0 =
           if Proofterm.export_standard_enabled () then
             Proof_Syntax.standard_proof_of
               {full = true, expand_name = SOME o expand_name thm_id} thm
           else if Proofterm.export_enabled () then Thm.reconstruct_proof_of thm
           else MinProof;
-        val (prop, SOME proof) =
-          standard_prop Name.context (Thm.extra_shyps thm) (Thm.full_prop_of thm) (SOME proof0);
+        val (prop, SOME proof) = standard_prop_of thm (SOME proof0);
         val _ = Thm.expose_proofs thy [thm];
       in
         (prop, deps, proof) |>
           let
             open XML.Encode Term_XML.Encode;

 
     val _ =
       if null constdefs then () else export_body thy "constdefs" (encode_constdefs constdefs);
 
 
+    (* spec rules *)
+
+    fun encode_spec {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 string (pair Spec_Rules.encode_rough_classification
+          (pair (list encode_term) (list encode_prop)))
+          (name, (rough_classification, (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));
+
+
     (* parents *)
 
     val _ =
       Export.export thy \<^path_binding>\<open>theory/parents\<close>
         (XML.Encode.string (cat_lines (map Context.theory_long_name parents)));