# HG changeset patch
# User berghofe
# Date 1184147920 -7200
# Node ID a0e7305dd0cbc113b8fcde3ea03fe54f639e9795
# Parent  742be2833ccd680f21b71fc7d0e3bca3a19122dc
Added function rew_proof (for pre-normalizing proofs).

diff -r 742be2833ccd -r a0e7305dd0cb src/Pure/proofterm.ML
--- a/src/Pure/proofterm.ML	Wed Jul 11 11:56:59 2007 +0200
+++ b/src/Pure/proofterm.ML	Wed Jul 11 11:58:40 2007 +0200
@@ -110,6 +110,7 @@
     (string * (typ list -> proof -> proof option)) list -> proof -> proof
   val rewrite_proof_notypes : (proof * proof) list *
     (string * (typ list -> proof -> proof option)) list -> proof -> proof
+  val rew_proof : theory -> proof -> proof
 end
 
 structure Proofterm : PROOFTERM =
@@ -1192,6 +1193,8 @@
       AList.merge (op =) (K true) (procs1, procs2));
 );
 
+fun rew_proof thy = rewrite_prf fst (ProofData.get thy);
+
 fun add_prf_rrule r = (ProofData.map o apfst) (insert (op =) r);
 
 fun add_prf_rproc p = (ProofData.map o apsnd) (AList.update (op =) p);