# HG changeset patch
# User wenzelm
# Date 1564126502 -7200
# Node ID 64ead6de6212643f14a46d8e14e8dc5c66e16054
# Parent  c533bec6e92d4ae56204ede744334ae0d8563844
defer rew_proof on unnamed PThm node as open_proof operation: significant performance improvement;
misc tuning and clarification;

diff -r c533bec6e92d -r 64ead6de6212 src/HOL/Tools/inductive_realizer.ML
--- a/src/HOL/Tools/inductive_realizer.ML	Thu Jul 25 14:01:06 2019 +0200
+++ b/src/HOL/Tools/inductive_realizer.ML	Fri Jul 26 09:35:02 2019 +0200
@@ -14,7 +14,7 @@
 struct
 
 fun name_of_thm thm =
-  (case Proofterm.fold_proof_atoms false (fn PThm (_, ((name, _, _), _)) => cons name | _ => I)
+  (case Proofterm.fold_proof_atoms false (fn PThm (_, ((name, _, _, _), _)) => cons name | _ => I)
       [Thm.proof_of thm] [] of
     [name] => name
   | _ => raise THM ("name_of_thm: bad proof of theorem", 0, [thm]));
diff -r c533bec6e92d -r 64ead6de6212 src/HOL/Tools/rewrite_hol_proof.ML
--- a/src/HOL/Tools/rewrite_hol_proof.ML	Thu Jul 25 14:01:06 2019 +0200
+++ b/src/HOL/Tools/rewrite_hol_proof.ML	Fri Jul 26 09:35:02 2019 +0200
@@ -305,9 +305,9 @@
 
 (** Replace congruence rules by substitution rules **)
 
-fun strip_cong ps (PThm (_, (("HOL.cong", _, _), _)) % _ % _ % SOME x % SOME y %%
+fun strip_cong ps (PThm (_, (("HOL.cong", _, _, _), _)) % _ % _ % SOME x % SOME y %%
       prfa %% prfT %% prf1 %% prf2) = strip_cong (((x, y), (prf2, prfa)) :: ps) prf1
-  | strip_cong ps (PThm (_, (("HOL.refl", _, _), _)) % SOME f %% _) = SOME (f, ps)
+  | strip_cong ps (PThm (_, (("HOL.refl", _, _, _), _)) % SOME f %% _) = SOME (f, ps)
   | strip_cong _ _ = NONE;
 
 val subst_prf = fst (Proofterm.strip_combt (fst (Proofterm.strip_combP (Thm.proof_of subst))));
@@ -330,15 +330,15 @@
 
 fun mk_AbsP P t = AbsP ("H", Option.map HOLogic.mk_Trueprop P, t);
 
-fun elim_cong_aux Ts (PThm (_, (("HOL.iffD1", _, _), _)) % _ % _ %% prf1 %% prf2) =
+fun elim_cong_aux Ts (PThm (_, (("HOL.iffD1", _, _, _), _)) % _ % _ %% prf1 %% prf2) =
       Option.map (make_subst Ts prf2 []) (strip_cong [] prf1)
-  | elim_cong_aux Ts (PThm (_, (("HOL.iffD1", _, _), _)) % P % _ %% prf) =
+  | elim_cong_aux Ts (PThm (_, (("HOL.iffD1", _, _, _), _)) % P % _ %% prf) =
       Option.map (mk_AbsP P o make_subst Ts (PBound 0) [])
         (strip_cong [] (Proofterm.incr_pboundvars 1 0 prf))
-  | elim_cong_aux Ts (PThm (_, (("HOL.iffD2", _, _), _)) % _ % _ %% prf1 %% prf2) =
+  | elim_cong_aux Ts (PThm (_, (("HOL.iffD2", _, _, _), _)) % _ % _ %% prf1 %% prf2) =
       Option.map (make_subst Ts prf2 [] o
         apsnd (map (make_sym Ts))) (strip_cong [] prf1)
-  | elim_cong_aux Ts (PThm (_, (("HOL.iffD2", _, _), _)) % _ % P %% prf) =
+  | elim_cong_aux Ts (PThm (_, (("HOL.iffD2", _, _, _), _)) % _ % P %% prf) =
       Option.map (mk_AbsP P o make_subst Ts (PBound 0) [] o
         apsnd (map (make_sym Ts))) (strip_cong [] (Proofterm.incr_pboundvars 1 0 prf))
   | elim_cong_aux _ _ = NONE;
diff -r c533bec6e92d -r 64ead6de6212 src/Pure/Proof/extraction.ML
--- a/src/Pure/Proof/extraction.ML	Thu Jul 25 14:01:06 2019 +0200
+++ b/src/Pure/Proof/extraction.ML	Fri Jul 26 09:35:02 2019 +0200
@@ -596,9 +596,9 @@
               (corr_prf1 % u %% corr_prf2, defs2)
           end
 
-      | corr d vs ts Ts hs cs _ (prf0 as PThm (_, ((name, prop, SOME Ts'), body))) _ defs =
+      | corr d vs ts Ts hs cs _ (prf0 as PThm (_, ((name, prop, SOME Ts', open_proof), body))) _ defs =
           let
-            val prf = Proofterm.join_proof body;
+            val prf = Proofterm.join_proof body |> open_proof;
             val (vs', tye) = find_inst prop Ts ts vs;
             val shyps = mk_shyps tye;
             val sprfs = mk_sprfs cs tye;
@@ -624,7 +624,7 @@
                     val corr_prf' =
                       Proofterm.proof_combP (Proofterm.proof_combt
                          (PThm (serial (),
-                          ((corr_name name vs', corr_prop, SOME (map TVar (Term.add_tvars corr_prop [] |> rev))),
+                          ((corr_name name vs', corr_prop, SOME (map TVar (Term.add_tvars corr_prop [] |> rev)), I),
                             Future.value (Proofterm.approximate_proof_body corr_prf))),
                               vfs_of corr_prop),
                               map PBound (length shyps - 1 downto 0)) |>
@@ -694,9 +694,9 @@
               in (f $ t, defs'') end
           end
 
-      | extr d vs ts Ts hs (prf0 as PThm (_, ((s, prop, SOME Ts'), body))) defs =
+      | extr d vs ts Ts hs (prf0 as PThm (_, ((s, prop, SOME Ts', open_proof), body))) defs =
           let
-            val prf = Proofterm.join_proof body;
+            val prf = Proofterm.join_proof body |> open_proof;
             val (vs', tye) = find_inst prop Ts ts vs;
             val shyps = mk_shyps tye;
             val tye' = (map fst (Term.add_tvars prop [] |> rev) ~~ Ts') @ tye
@@ -741,7 +741,7 @@
                     val corr_prf'' =
                       Proofterm.proof_combP (Proofterm.proof_combt
                         (PThm (serial (),
-                         ((corr_name s vs', corr_prop, SOME (map TVar (Term.add_tvars corr_prop [] |> rev))),
+                         ((corr_name s vs', corr_prop, SOME (map TVar (Term.add_tvars corr_prop [] |> rev)), I),
                            Future.value (Proofterm.approximate_proof_body corr_prf'))),
                             vfs_of corr_prop),
                              map PBound (length shyps - 1 downto 0)) |>
diff -r c533bec6e92d -r 64ead6de6212 src/Pure/Proof/proof_checker.ML
--- a/src/Pure/Proof/proof_checker.ML	Thu Jul 25 14:01:06 2019 +0200
+++ b/src/Pure/Proof/proof_checker.ML	Fri Jul 26 09:35:02 2019 +0200
@@ -84,7 +84,7 @@
             Thm.instantiate (ctye, []) (forall_intr_vars (Thm.forall_intr_frees thm'))
           end;
 
-        fun thm_of _ _ (PThm (_, ((name, prop', SOME Ts), _))) =
+        fun thm_of _ _ (PThm (_, ((name, prop', SOME Ts, _), _))) =
               let
                 val thm = Thm.unconstrainT (Drule.implies_intr_hyps (lookup name));
                 val prop = Thm.prop_of thm;
diff -r c533bec6e92d -r 64ead6de6212 src/Pure/Proof/proof_rewrite_rules.ML
--- a/src/Pure/Proof/proof_rewrite_rules.ML	Thu Jul 25 14:01:06 2019 +0200
+++ b/src/Pure/Proof/proof_rewrite_rules.ML	Fri Jul 26 09:35:02 2019 +0200
@@ -35,12 +35,12 @@
     val equal_elim_axm = ax Proofterm.equal_elim_axm [];
     val symmetric_axm = ax Proofterm.symmetric_axm [propT];
 
-    fun rew' (PThm (_, (("Pure.protectD", _, _), _)) % _ %%
-        (PThm (_, (("Pure.protectI", _, _), _)) % _ %% prf)) = SOME prf
-      | rew' (PThm (_, (("Pure.conjunctionD1", _, _), _)) % _ % _ %%
-        (PThm (_, (("Pure.conjunctionI", _, _), _)) % _ % _ %% prf %% _)) = SOME prf
-      | rew' (PThm (_, (("Pure.conjunctionD2", _, _), _)) % _ % _ %%
-        (PThm (_, (("Pure.conjunctionI", _, _), _)) % _ % _ %% _ %% prf)) = SOME prf
+    fun rew' (PThm (_, (("Pure.protectD", _, _, _), _)) % _ %%
+        (PThm (_, (("Pure.protectI", _, _, _), _)) % _ %% prf)) = SOME prf
+      | rew' (PThm (_, (("Pure.conjunctionD1", _, _, _), _)) % _ % _ %%
+        (PThm (_, (("Pure.conjunctionI", _, _, _), _)) % _ % _ %% prf %% _)) = SOME prf
+      | rew' (PThm (_, (("Pure.conjunctionD2", _, _, _), _)) % _ % _ %%
+        (PThm (_, (("Pure.conjunctionI", _, _, _), _)) % _ % _ %% _ %% prf)) = SOME prf
       | rew' (PAxm ("Pure.equal_elim", _, _) % _ % _ %%
         (PAxm ("Pure.equal_intr", _, _) % _ % _ %% prf %% _)) = SOME prf
       | rew' (PAxm ("Pure.symmetric", _, _) % _ % _ %%
@@ -50,14 +50,14 @@
       | rew' (PAxm ("Pure.equal_elim", _, _) % SOME (_ $ A) % SOME (_ $ B) %%
         (PAxm ("Pure.combination", _, _) % SOME (Const ("Pure.prop", _)) %
           _ % _ % _ %% (PAxm ("Pure.reflexive", _, _) % _) %% prf1) %%
-        ((tg as PThm (_, (("Pure.protectI", _, _), _))) % _ %% prf2)) =
+        ((tg as PThm (_, (("Pure.protectI", _, _, _), _))) % _ %% prf2)) =
         SOME (tg %> B %% (equal_elim_axm %> A %> B %% prf1 %% prf2))
 
       | rew' (PAxm ("Pure.equal_elim", _, _) % SOME (_ $ A) % SOME (_ $ B) %%
         (PAxm ("Pure.symmetric", _, _) % _ % _ %%
           (PAxm ("Pure.combination", _, _) % SOME (Const ("Pure.prop", _)) %
              _ % _ % _ %% (PAxm ("Pure.reflexive", _, _) % _) %% prf1)) %%
-        ((tg as PThm (_, (("Pure.protectI", _, _), _))) % _ %% prf2)) =
+        ((tg as PThm (_, (("Pure.protectI", _, _, _), _))) % _ %% prf2)) =
         SOME (tg %> B %% (equal_elim_axm %> A %> B %%
           (symmetric_axm % ?? B % ?? A %% prf1) %% prf2))
 
@@ -233,7 +233,7 @@
       (AbsP (s, t, fst (insert_refl defs Ts prf)), false)
   | insert_refl defs Ts prf =
       (case Proofterm.strip_combt prf of
-        (PThm (_, ((s, prop, SOME Ts), _)), ts) =>
+        (PThm (_, ((s, prop, SOME Ts, _), _)), ts) =>
           if member (op =) defs s then
             let
               val vs = vars_of prop;
@@ -259,7 +259,7 @@
       let
         val cnames = map (fst o dest_Const o fst) defs';
         val thms = Proofterm.fold_proof_atoms true
-          (fn PThm (_, ((name, prop, _), _)) =>
+          (fn PThm (_, ((name, prop, _, _), _)) =>
               if member (op =) defnames name orelse
                 not (exists_Const (member (op =) cnames o #1) prop)
               then I
diff -r c533bec6e92d -r 64ead6de6212 src/Pure/Proof/proof_syntax.ML
--- a/src/Pure/Proof/proof_syntax.ML	Thu Jul 25 14:01:06 2019 +0200
+++ b/src/Pure/Proof/proof_syntax.ML	Fri Jul 26 09:35:02 2019 +0200
@@ -167,7 +167,7 @@
 fun proof_syntax prf =
   let
     val thm_names = Symtab.keys (Proofterm.fold_proof_atoms true
-      (fn PThm (_, ((name, _, _), _)) => if name <> "" then Symtab.update (name, ()) else I
+      (fn PThm (_, ((name, _, _, _), _)) => if name <> "" then Symtab.update (name, ()) else I
         | _ => I) [prf] Symtab.empty);
     val axm_names = Symtab.keys (Proofterm.fold_proof_atoms true
       (fn PAxm (name, _, _) => Symtab.update (name, ()) | _ => I) [prf] Symtab.empty);
@@ -184,7 +184,7 @@
     val prf = Thm.proof_of thm;
     val prf' =
       (case Proofterm.strip_combt (fst (Proofterm.strip_combP prf)) of
-        (PThm (_, ((_, prop', _), body)), _) =>
+        (PThm (_, ((_, prop', _, _), body)), _) =>
           if prop = prop' then Proofterm.join_proof body else prf
       | _ => prf)
   in if full then Reconstruct.reconstruct_proof ctxt prop prf' else prf' end;
diff -r c533bec6e92d -r 64ead6de6212 src/Pure/Proof/reconstruct.ML
--- a/src/Pure/Proof/reconstruct.ML	Thu Jul 25 14:01:06 2019 +0200
+++ b/src/Pure/Proof/reconstruct.ML	Fri Jul 26 09:35:02 2019 +0200
@@ -209,7 +209,7 @@
                  add_cnstrt Ts (v $ t) (prf % SOME t) cnstrts env3 vTs'
                    (u, Const ("Pure.all", (T --> propT) --> propT) $ v)
                end)
-      | mk_cnstrts env _ _ vTs (prf as PThm (_, ((_, prop, opTs), _))) =
+      | mk_cnstrts env _ _ vTs (prf as PThm (_, ((_, prop, opTs, _), _))) =
           mk_cnstrts_atom env vTs prop opTs prf
       | mk_cnstrts env _ _ vTs (prf as PAxm (_, prop, opTs)) =
           mk_cnstrts_atom env vTs prop opTs prf
@@ -312,7 +312,7 @@
       Const ("Pure.imp", _) $ P $ Q => Q
     | _ => error "prop_of: ==> expected")
   | prop_of0 Hs (Hyp t) = t
-  | prop_of0 Hs (PThm (_, ((_, prop, SOME Ts), _))) = prop_of_atom prop Ts
+  | prop_of0 Hs (PThm (_, ((_, prop, SOME Ts, _), _))) = prop_of_atom prop Ts
   | prop_of0 Hs (PAxm (_, prop, SOME Ts)) = prop_of_atom prop Ts
   | prop_of0 Hs (OfClass (T, c)) = Logic.mk_of_class (T, c)
   | prop_of0 Hs (Oracle (_, prop, SOME Ts)) = prop_of_atom prop Ts
@@ -330,6 +330,8 @@
 
 fun expand_proof ctxt thms prf =
   let
+    val thy = Proof_Context.theory_of ctxt;
+
     fun expand maxidx prfs (AbsP (s, t, prf)) =
           let val (maxidx', prfs', prf') = expand maxidx prfs prf
           in (maxidx', prfs', AbsP (s, t, prf')) end
@@ -344,7 +346,7 @@
       | expand maxidx prfs (prf % t) =
           let val (maxidx', prfs', prf') = expand maxidx prfs prf
           in (maxidx', prfs', prf' % t) end
-      | expand maxidx prfs (prf as PThm (_, ((a, prop, SOME Ts), body))) =
+      | expand maxidx prfs (prf as PThm (_, ((a, prop, SOME Ts, open_proof), body))) =
           if not (exists
             (fn (b, NONE) => a = b
               | (b, SOME prop') => a = b andalso prop = prop') thms)
@@ -357,8 +359,11 @@
                     val _ =
                       message ctxt (fn () =>
                         "Reconstructing proof of " ^ a ^ "\n" ^ Syntax.string_of_term ctxt prop);
-                    val prf' = Proofterm.forall_intr_vfs_prf prop
-                      (reconstruct_proof ctxt prop (Proofterm.join_proof body));
+                    val prf' =
+                      Proofterm.join_proof body
+                      |> open_proof
+                      |> reconstruct_proof ctxt prop
+                      |> Proofterm.forall_intr_vfs_prf prop;
                     val (maxidx', prfs', prf) = expand
                       (Proofterm.maxidx_proof prf' ~1) prfs prf'
                   in (maxidx' + maxidx + 1, Proofterm.incr_indexes (maxidx + 1) prf,
diff -r c533bec6e92d -r 64ead6de6212 src/Pure/proofterm.ML
--- a/src/Pure/proofterm.ML	Thu Jul 25 14:01:06 2019 +0200
+++ b/src/Pure/proofterm.ML	Fri Jul 26 09:35:02 2019 +0200
@@ -20,7 +20,7 @@
    | PAxm of string * term * typ list option
    | OfClass of typ * class
    | Oracle of string * term * typ list option
-   | PThm of serial * ((string * term * typ list option) * proof_body future)
+   | PThm of serial * ((string * term * typ list option * (proof -> proof)) * proof_body future)
   and proof_body = PBody of
     {oracles: (string * term) Ord_List.T,
      thms: (serial * thm_node) Ord_List.T,
@@ -178,7 +178,7 @@
  | PAxm of string * term * typ list option
  | OfClass of typ * class
  | Oracle of string * term * typ list option
- | PThm of serial * ((string * term * typ list option) * proof_body future)
+ | PThm of serial * ((string * term * typ list option * (proof -> proof)) * proof_body future)
 and proof_body = PBody of
   {oracles: (string * term) Ord_List.T,
    thms: (serial * thm_node) Ord_List.T,
@@ -295,7 +295,7 @@
   let
     val (oracles, thms) = fold_proof_atoms false
       (fn Oracle (s, prop, _) => apfst (cons (s, prop))
-        | PThm (i, ((name, prop, _), body)) => apsnd (cons (i, make_thm_node name prop body))
+        | PThm (i, ((name, prop, _, _), body)) => apsnd (cons (i, make_thm_node name prop body))
         | _ => I) [prf] ([], []);
   in
     PBody
@@ -335,8 +335,9 @@
   fn PAxm (a, b, c) => ([a], pair term (option (list typ)) (b, c)),
   fn OfClass (a, b) => ([b], typ a),
   fn Oracle (a, b, c) => ([a], pair term (option (list typ)) (b, c)),
-  fn PThm (a, ((b, c, d), body)) =>
-    ([int_atom a, b], triple term (option (list typ)) proof_body (c, d, Future.join body))]
+  fn PThm (a, ((b, c, d, open_proof), body)) =>
+    ([int_atom a, b], triple term (option (list typ)) proof_body
+      (c, d, map_proof_of open_proof (Future.join body)))]
 and proof_body (PBody {oracles, thms, proof = prf}) =
   triple (list (pair string term)) (list pthm) proof (oracles, thms, prf)
 and pthm (a, thm_node) =
@@ -370,7 +371,7 @@
   fn ([a], b) => let val (c, d) = pair term (option (list typ)) b in Oracle (a, c, d) end,
   fn ([a, b], c) =>
     let val (d, e, f) = triple term (option (list typ)) proof_body c
-    in PThm (int_atom a, ((b, d, e), Future.value f)) end]
+    in PThm (int_atom a, ((b, d, e, I), Future.value f)) end]
 and proof_body x =
   let val (a, b, c) = triple (list (pair string term)) (list pthm) proof x
   in PBody {oracles = a, thms = b, proof = c} end
@@ -444,8 +445,8 @@
       | proof (PAxm (a, prop, SOME Ts)) = PAxm (a, prop, SOME (typs Ts))
       | proof (OfClass T_c) = ofclass T_c
       | proof (Oracle (a, prop, SOME Ts)) = Oracle (a, prop, SOME (typs Ts))
-      | proof (PThm (i, ((a, prop, SOME Ts), body))) =
-          PThm (i, ((a, prop, SOME (typs Ts)), body))
+      | proof (PThm (i, ((a, prop, SOME Ts, open_proof), body))) =
+          PThm (i, ((a, prop, SOME (typs Ts), open_proof), body))
       | proof _ = raise Same.SAME;
   in proof end;
 
@@ -470,7 +471,7 @@
   | fold_proof_terms _ g (PAxm (_, _, SOME Ts)) = fold g Ts
   | fold_proof_terms _ g (OfClass (T, _)) = g T
   | fold_proof_terms _ g (Oracle (_, _, SOME Ts)) = fold g Ts
-  | fold_proof_terms _ g (PThm (_, ((_, _, SOME Ts), _))) = fold g Ts
+  | fold_proof_terms _ g (PThm (_, ((_, _, SOME Ts, _), _))) = fold g Ts
   | fold_proof_terms _ _ _ = I;
 
 fun maxidx_proof prf = fold_proof_terms Term.maxidx_term Term.maxidx_typ prf;
@@ -484,8 +485,8 @@
 fun change_type opTs (PAxm (name, prop, _)) = PAxm (name, prop, opTs)
   | change_type (SOME [T]) (OfClass (_, c)) = OfClass (T, c)
   | change_type opTs (Oracle (name, prop, _)) = Oracle (name, prop, opTs)
-  | change_type opTs (PThm (i, ((name, prop, _), body))) =
-      PThm (i, ((name, prop, opTs), body))
+  | change_type opTs (PThm (i, ((name, prop, _, open_proof), body))) =
+      PThm (i, ((name, prop, opTs, open_proof), body))
   | change_type _ prf = prf;
 
 
@@ -632,8 +633,8 @@
           OfClass (htypeT Envir.norm_type_same T, c)
       | norm (Oracle (s, prop, Ts)) =
           Oracle (s, prop, Same.map_option (htypeTs Envir.norm_types_same) Ts)
-      | norm (PThm (i, ((s, t, Ts), body))) =
-          PThm (i, ((s, t, Same.map_option (htypeTs Envir.norm_types_same) Ts), body))
+      | norm (PThm (i, ((s, t, Ts, open_proof), body))) =
+          PThm (i, ((s, t, Same.map_option (htypeTs Envir.norm_types_same) Ts, open_proof), body))
       | norm _ = raise Same.SAME;
   in Same.commit norm end;
 
@@ -776,7 +777,7 @@
   let val U = Term.itselfT T --> propT
   in Const ("Pure.OfClass", U --> proofT) $ Const (Logic.const_of_class c, U) end;
 
-fun term_of _ (PThm (_, ((name, _, Ts), _))) =
+fun term_of _ (PThm (_, ((name, _, Ts, _), _))) =
       fold AppT (these Ts) (Const (Long_Name.append "thm" name, proofT))
   | term_of _ (PAxm (name, _, Ts)) =
       fold AppT (these Ts) (Const (Long_Name.append "axm" name, proofT))
@@ -949,8 +950,8 @@
           OfClass (Logic.incr_tvar_same inc T, c)
       | lift' _ _ (Oracle (s, prop, Ts)) =
           Oracle (s, prop, (Same.map_option o Same.map) (Logic.incr_tvar_same inc) Ts)
-      | lift' _ _ (PThm (i, ((s, prop, Ts), body))) =
-          PThm (i, ((s, prop, (Same.map_option o Same.map) (Logic.incr_tvar inc) Ts), body))
+      | lift' _ _ (PThm (i, ((s, prop, Ts, open_proof), body))) =
+          PThm (i, ((s, prop, (Same.map_option o Same.map) (Logic.incr_tvar inc) Ts, open_proof), body))
       | lift' _ _ _ = raise Same.SAME
     and lifth' Us Ts prf = (lift' Us Ts prf handle Same.SAME => prf);
 
@@ -1287,7 +1288,7 @@
               (case prf of
                 PAxm (_, prop, _) => prop
               | Oracle (_, prop, _) => prop
-              | PThm (_, ((_, prop, _), _)) => prop
+              | PThm (_, ((_, prop, _, _), _)) => prop
               | _ => raise Fail "shrink: proof not in normal form");
             val vs = vars_of prop;
             val (ts', ts'') = chop (length vs) ts;
@@ -1376,7 +1377,8 @@
       | mtch Ts i j inst (OfClass (T1, c1), OfClass (T2, c2)) =
           if c1 = c2 then matchT inst (T1, T2)
           else raise PMatch
-      | mtch Ts i j inst (PThm (_, ((name1, prop1, opTs), _)), PThm (_, ((name2, prop2, opUs), _))) =
+      | mtch Ts i j inst
+            (PThm (_, ((name1, prop1, opTs, _), _)), PThm (_, ((name2, prop2, opUs, _), _))) =
           if name1 = name2 andalso prop1 = prop2 then
             optmatch matchTs inst (opTs, opUs)
           else raise PMatch
@@ -1422,8 +1424,8 @@
       | subst _ _ (PAxm (id, prop, Ts)) = PAxm (id, prop, Same.map_option substTs Ts)
       | subst _ _ (OfClass (T, c)) = OfClass (substT T, c)
       | subst _ _ (Oracle (id, prop, Ts)) = Oracle (id, prop, Same.map_option substTs Ts)
-      | subst _ _ (PThm (i, ((id, prop, Ts), body))) =
-          PThm (i, ((id, prop, Same.map_option substTs Ts), body))
+      | subst _ _ (PThm (i, ((id, prop, Ts, open_proof), body))) =
+          PThm (i, ((id, prop, Same.map_option substTs Ts, open_proof), body))
       | subst _ _ _ = raise Same.SAME;
   in fn t => subst 0 0 t handle Same.SAME => t end;
 
@@ -1447,7 +1449,7 @@
       | (Hyp (Var _), _) => true
       | (PAxm (a, _, _), PAxm (b, _, _)) => a = b andalso matchrands prf1 prf2
       | (OfClass (_, c), OfClass (_, d)) => c = d andalso matchrands prf1 prf2
-      | (PThm (_, ((a, propa, _), _)), PThm (_, ((b, propb, _), _))) =>
+      | (PThm (_, ((a, propa, _, _), _)), PThm (_, ((b, propb, _, _), _))) =>
           a = b andalso propa = propb andalso matchrands prf1 prf2
       | (PBound i, PBound j) => i = j andalso matchrands prf1 prf2
       | (AbsP _, _) =>  true   (*because of possible eta equality*)
@@ -1603,7 +1605,7 @@
       | clean maxidx prfs (prf % t) =
           let val (maxidx', prfs', prf') = clean maxidx prfs prf
           in (maxidx', prfs', prf' % t) end
-      | clean maxidx prfs (PThm (_, (("", prop, SOME Ts), body))) =
+      | clean maxidx prfs (PThm (_, (("", prop, SOME Ts, _), body))) =
           let
             val (maxidx', prf, prfs') =
               (case AList.lookup (op =) prfs prop of
@@ -1707,47 +1709,39 @@
 
     fun make_body0 proof0 = PBody {oracles = oracles0, thms = thms0, proof = proof0};
     val body0 =
-      if not (proofs_enabled ()) then Future.value (make_body0 MinProof)
-      else
-        let
-          val rew = rew_proof thy;
-          val prf0 = fold_rev implies_intr_proof hyps prf;
-        in
-          (singleton o Future.cond_forks)
-            {name = "Proofterm.prepare_thm_proof", group = NONE,
-              deps = [], pri = 1, interrupts = true}
-            (fn () => make_body0 (rew prf0))
-        end;
+      Future.value (make_body0
+        (if proofs_enabled () then fold_rev implies_intr_proof hyps prf else MinProof))
 
     fun export i prf1 =
-     if Options.default_bool "export_proofs" then
+      if Options.default_bool "export_proofs" then
         Export.export thy (Path.binding0 (Path.make ["proofs", string_of_int i]))
-          (Buffer.chunks
-            (YXML.buffer_body (Term_XML.Encode.term (term_of_proof prf1)) Buffer.empty))
+          (Buffer.chunks (YXML.buffer_body (Term_XML.Encode.term (term_of_proof prf1)) Buffer.empty))
       else ();
 
     fun prune prf1 =
-      if Options.default_bool "prune_proofs" then MinProof else shrink_proof prf1;
+      if Options.default_bool "prune_proofs" then MinProof
+      else shrink_proof prf1;
 
-    fun publish i = tap (export i) #> prune;
+    fun publish i = clean_proof thy #> tap (export i) #> prune;
 
     fun new_prf () =
       let
         val i = proof_serial ();
         val postproc =
           unconstrainT_body thy (atyp_map, constraints) #>
-          name <> "" ? map_proof_of (clean_proof thy #> publish i);
+          name <> "" ? map_proof_of (publish i);
       in (i, fulfill_proof_future thy promises postproc body0) end;
 
     val (i, body') =
       (*non-deterministic, depends on unknown promises*)
       (case strip_combt (fst (strip_combP prf)) of
-        (PThm (i, ((a, prop', NONE), body')), args') =>
+        (PThm (i, ((a, prop', NONE, _), body')), args') =>
           if (a = "" orelse a = name) andalso prop1 = prop' andalso args = args'
           then (i, body' |> (a = "" andalso name <> "") ? Future.map (map_proof_of (publish i)))
           else new_prf ()
       | _ => new_prf ());
-    val head = PThm (i, ((name, prop1, NONE), body'));
+    val open_proof = if name = "" then clean_proof thy #> shrink_proof else I;
+    val head = PThm (i, ((name, prop1, NONE, open_proof), body'));
   in ((i, make_thm_node name prop1 body'), head, args, argsP, args1) end;
 
 fun thm_proof thy name shyps hyps concl promises body =
@@ -1762,11 +1756,11 @@
 fun get_name shyps hyps prop prf =
   let val (_, prop) = Logic.unconstrainT shyps (Logic.list_implies (hyps, prop)) in
     (case strip_combt (fst (strip_combP prf)) of
-      (PThm (_, ((name, prop', _), _)), _) => if prop = prop' then name else ""
+      (PThm (_, ((name, prop', _, _), _)), _) => if prop = prop' then name else ""
     | _ => "")
   end;
 
-fun guess_name (PThm (_, ((name, _, _), _))) = name
+fun guess_name (PThm (_, ((name, _, _, _), _))) = name
   | guess_name (prf %% Hyp _) = guess_name prf
   | guess_name (prf %% OfClass _) = guess_name prf
   | guess_name (prf % NONE) = guess_name prf