# HG changeset patch
# User wenzelm
# Date 1571600069 -7200
# Node ID 693e811b91bb6bdeece45876ab894cddca661987
# Parent  4c15217d6266019bb9560e3d901131b91d866e3a
more robust hybrid treatment of Pure, notably for Isabelle/Dedukti;

diff -r 4c15217d6266 -r 693e811b91bb src/Pure/ROOT
--- a/src/Pure/ROOT	Sun Oct 20 21:12:18 2019 +0200
+++ b/src/Pure/ROOT	Sun Oct 20 21:34:29 2019 +0200
@@ -4,7 +4,7 @@
   description "
     The Pure logical framework.
   "
-  options [threads = 1, export_proofs, export_standard_proofs]
+  options [threads = 1, export_proofs, export_standard_proofs, prune_proofs = false]
   theories [export_theory]
     Pure (global)
   theories
diff -r 4c15217d6266 -r 693e811b91bb src/Pure/Thy/export_theory.ML
--- a/src/Pure/Thy/export_theory.ML	Sun Oct 20 21:12:18 2019 +0200
+++ b/src/Pure/Thy/export_theory.ML	Sun Oct 20 21:34:29 2019 +0200
@@ -255,13 +255,11 @@
     val lookup_thm_id = Global_Theory.lookup_thm_id thy;
 
     fun proof_boxes_of thm thm_id =
-      if export_standard_proofs then []
-      else
-        let
-          val dep_boxes =
-            thm |> Thm_Deps.proof_boxes (fn thm_id' =>
-              if #serial thm_id = #serial thm_id' then false else is_some (lookup_thm_id thm_id'));
-        in dep_boxes @ [thm_id] end;
+      let
+        val dep_boxes =
+          thm |> Thm_Deps.proof_boxes (fn thm_id' =>
+            if #serial thm_id = #serial thm_id' then false else is_some (lookup_thm_id thm_id'));
+      in dep_boxes @ [thm_id] end;
 
     fun expand_name thm_id (header: Proofterm.thm_header) =
       if #serial header = #serial thm_id then ""