# HG changeset patch
# User wenzelm
# Date 1563962048 -7200
# Node ID 64fdd75c1dea0341da0814cb207b2ea146eb997a
# Parent  9dc99e3153b321f7ead2d47e3746e0b6efc91063
more thorough clean_proof;

diff -r 9dc99e3153b3 -r 64fdd75c1dea src/Pure/proofterm.ML
--- a/src/Pure/proofterm.ML	Wed Jul 24 11:32:18 2019 +0200
+++ b/src/Pure/proofterm.ML	Wed Jul 24 11:54:08 2019 +0200
@@ -151,7 +151,7 @@
 
   val forall_intr_vfs: term -> term
   val forall_intr_vfs_prf: term -> proof -> proof
-  val clean_proof: proof -> proof
+  val clean_proof: theory -> proof -> proof
 
   val fulfill_norm_proof: theory -> (serial * proof_body) list -> proof_body -> proof_body
   val thm_proof: theory -> string -> sort list -> term list -> term ->
@@ -1587,7 +1587,7 @@
 
 end;
 
-fun clean_proof prf =
+fun clean_proof thy prf =
   let
     fun clean maxidx prfs (AbsP (s, t, prf)) =
           let val (maxidx', prfs', prf') = clean maxidx prfs prf
@@ -1624,8 +1624,7 @@
           end
       | clean maxidx prfs prf = (maxidx, prfs, prf);
 
-    val maxidx = maxidx_proof prf ~1;
-  in norm_proof (Envir.empty maxidx) (#3 (clean maxidx [] prf)) end;
+  in rew_proof thy (#3 (clean (maxidx_proof prf ~1) [] prf)) end;
 
 
 
@@ -1726,7 +1725,7 @@
       else ();
       if Options.default_bool "prune_proofs" then MinProof else prf1);
 
-    fun publish i = clean_proof #> export i #> shrink_proof;
+    fun publish i = clean_proof thy #> export i #> shrink_proof;
 
     fun new_prf () =
       let