# HG changeset patch
# User berghofe
# Date 1184147961 -7200
# Node ID ab793a6ddf9fc38cd9672a2c530b25516bc46168
# Parent  a0e7305dd0cbc113b8fcde3ea03fe54f639e9795
Added function norm_proof for normalizing the proof term
corresponding to a theorem.

diff -r a0e7305dd0cb -r ab793a6ddf9f src/Pure/thm.ML
--- a/src/Pure/thm.ML	Wed Jul 11 11:58:40 2007 +0200
+++ b/src/Pure/thm.ML	Wed Jul 11 11:59:21 2007 +0200
@@ -141,6 +141,7 @@
   val get_tags: thm -> Markup.property list
   val map_tags: (Markup.property list -> Markup.property list) -> thm -> thm
   val compress: thm -> thm
+  val norm_proof: thm -> thm
   val adjust_maxidx_thm: int -> thm -> thm
   val rename_boundvars: term -> term -> thm -> thm
   val match: cterm * cterm -> (ctyp * ctyp) list * (cterm * cterm) list
@@ -584,6 +585,18 @@
       prop = Compress.term thy prop}
   end;
 
+fun norm_proof (Thm {thy_ref, der, tags, maxidx, shyps, hyps, tpairs, prop}) =
+  let val thy = Theory.deref thy_ref in
+    Thm {thy_ref = thy_ref,
+      der = Pt.infer_derivs' (Pt.rew_proof thy) der,
+      tags = tags,
+      maxidx = maxidx,
+      shyps = shyps,
+      hyps = hyps,
+      tpairs = tpairs,
+      prop = prop}
+  end;
+
 fun adjust_maxidx_thm i (th as Thm {thy_ref, der, tags, maxidx, shyps, hyps, tpairs, prop}) =
   if maxidx = i then th
   else if maxidx < i then