# HG changeset patch
# User wenzelm
# Date 1564477972 -7200
# Node ID 6410166400ea5a15e02eee28f47c00912d4a08fb
# Parent  52435af442a66890ff9f0ba818376e7d032987d9
discontinue clean_proof: without type args its PThm nodes are not expanded, but with type args it is too unstable;

diff -r 52435af442a6 -r 6410166400ea src/Pure/proofterm.ML
--- a/src/Pure/proofterm.ML	Mon Jul 29 18:44:39 2019 +0200
+++ b/src/Pure/proofterm.ML	Tue Jul 30 11:12:52 2019 +0200
@@ -155,7 +155,6 @@
   val forall_intr_vfs: term -> term
   val forall_intr_vfs_prf: term -> proof -> proof
   val app_types: int -> term -> typ list -> proof -> proof
-  val clean_proof: theory -> proof -> proof
 
   val proof_serial: unit -> proof_serial
   val fulfill_norm_proof: theory -> (serial * proof_body) list -> proof_body -> proof_body
@@ -1613,38 +1612,6 @@
 
 end;
 
-fun clean_proof thy prf =
-  let
-    fun clean maxidx prfs (AbsP (s, t, prf)) =
-          let val (maxidx', prfs', prf') = clean maxidx prfs prf
-          in (maxidx', prfs', AbsP (s, t, prf')) end
-      | clean maxidx prfs (Abst (s, T, prf)) =
-          let val (maxidx', prfs', prf') = clean maxidx prfs prf
-          in (maxidx', prfs', Abst (s, T, prf')) end
-      | clean maxidx prfs (prf1 %% prf2) =
-          let
-            val (maxidx', prfs', prf1') = clean maxidx prfs prf1;
-            val (maxidx'', prfs'', prf2') = clean maxidx' prfs' prf2;
-          in (maxidx'', prfs'', prf1' %% prf2') end
-      | 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))) =
-          let
-            val (maxidx', prf, prfs') =
-              (case AList.lookup (op =) prfs prop of
-                NONE =>
-                  let
-                    val prf' = forall_intr_vfs_prf prop (join_proof body);
-                    val (maxidx', prfs', prf) = clean (maxidx_proof prf' ~1) prfs prf';
-                    val prfs'' = (prop, (maxidx', prf)) :: prfs';
-                  in (maxidx' + maxidx + 1, incr_indexes (maxidx + 1) prf, prfs'') end
-              | SOME (maxidx', prf) => (maxidx' + maxidx + 1, incr_indexes (maxidx + 1) prf, prfs));
-          in (maxidx', prfs', app_types (maxidx + 1) prop Ts prf) end
-      | clean maxidx prfs prf = (maxidx, prfs, prf);
-
-  in rew_proof thy (#3 (clean (maxidx_proof prf ~1) [] prf)) end;
-
 
 
 (** promises **)
@@ -1726,8 +1693,8 @@
         (PBody {oracles = oracles0, thms = thms0,
           proof = if proofs_enabled () then fold_rev implies_intr_proof hyps prf else MinProof});
 
-    fun publish i = map_proof_of (clean_proof thy #> tap (export thy i) #> prune);
-    val open_proof = not named ? (clean_proof thy #> shrink_proof);
+    fun publish i = map_proof_of (rew_proof thy #> tap (export thy i) #> prune);
+    val open_proof = not named ? (rew_proof thy #> shrink_proof);
 
     fun new_prf () =
       let