src/Pure/Thy/export_theory.ML

--- a/src/Pure/Thy/export_theory.ML	Thu Aug 15 16:02:47 2019 +0200
+++ b/src/Pure/Thy/export_theory.ML	Thu Aug 15 16:06:57 2019 +0200
@@ -220,40 +220,43 @@
 
     (* axioms and facts *)
 
-    fun prop_of raw_thm =
+    fun standard_prop used extra_shyps raw_prop raw_proof =
       let
-        val thm = raw_thm
-          |> Thm.transfer thy
-          |> Thm.check_hyps (Context.Theory thy)
-          |> Thm.strip_shyps;
-        val prop = thm
-          |> Thm.full_prop_of;
-      in (Thm.extra_shyps thm, prop) end;
+        val raw_proofs = the_list raw_proof;
+        val used_proofs = used |> fold Proofterm.used_frees_proof raw_proofs;
+        val ([prop], proofs) = ([raw_prop], raw_proofs) |> Proofterm.standard_vars used_proofs;
 
-    fun encode_prop used (Ss, raw_prop) =
-      let
-        val prop = Proofterm.standard_vars_term used raw_prop;
         val args = rev (add_frees used prop []);
         val typargs = rev (add_tfrees used prop []);
-        val used' = fold (Name.declare o #1) typargs used;
-        val sorts = Name.invent used' Name.aT (length Ss) ~~ Ss;
-      in
-        (sorts @ typargs, args, prop) |>
-          let open XML.Encode Term_XML.Encode
-          in triple (list (pair string sort)) (list (pair string typ)) term end
-      end;
+        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), try hd proofs) end;
+
+    val encode_prop =
+      let open XML.Encode Term_XML.Encode
+      in triple (list (pair string sort)) (list (pair string typ)) term end;
+
+    fun encode_axiom used prop =
+      encode_prop (#1 (standard_prop used [] prop NONE));
 
-    fun encode_axiom used t = encode_prop used ([], t);
+    val clean_thm =
+      Thm.transfer thy
+      #> Thm.check_hyps (Context.Theory thy)
+      #> Thm.strip_shyps;
 
-    val encode_fact = encode_prop Name.context;
-    val encode_fact_single = encode_fact o prop_of;
-    val encode_fact_multi = XML.Encode.list encode_fact o map prop_of;
+    val encode_fact = clean_thm #> (fn thm =>
+      standard_prop Name.context
+        (Thm.extra_shyps thm)
+        (Thm.full_prop_of thm)
+        (try Thm.reconstruct_proof_of thm) |>
+      let open XML.Encode Term_XML.Encode
+      in pair encode_prop (option Proofterm.encode_full) end);
 
     val _ =
       export_entities "axioms" (fn _ => fn t => SOME (encode_axiom Name.context t))
         Theory.axiom_space (Theory.axioms_of thy);
     val _ =
-      export_entities "facts" (K (SOME o encode_fact_multi))
+      export_entities "facts" (K (SOME o XML.Encode.list encode_fact))
         (Facts.space_of o Global_Theory.facts_of)
         (Facts.dest_static true [] (Global_Theory.facts_of thy));
 
@@ -262,12 +265,12 @@
 
     val encode_class =
       let open XML.Encode Term_XML.Encode
-      in pair (list (pair string typ)) (list encode_fact_single) end;
+      in pair (list (pair string typ)) (list (encode_axiom Name.context)) end;
 
     fun export_class name =
       (case try (Axclass.get_info thy) name of
         NONE => ([], [])
-      | SOME {params, axioms, ...} => (params, axioms))
+      | SOME {params, axioms, ...} => (params, map (Thm.plain_prop_of o clean_thm) axioms))
       |> encode_class |> SOME;
 
     val _ =