# HG changeset patch
# User wenzelm
# Date 1030439113 -7200
# Node ID bbd328200a9aefca9d92c138e394f2301d00dd8f
# Parent  9269275e5da682e5ca5ae531064d879428078025
thms/axms_of_proof: proper handling of MinProof;

diff -r 9269275e5da6 -r bbd328200a9a src/Pure/proofterm.ML
--- a/src/Pure/proofterm.ML	Tue Aug 27 11:04:27 2002 +0200
+++ b/src/Pure/proofterm.ML	Tue Aug 27 11:05:13 2002 +0200
@@ -155,6 +155,7 @@
          None => thms_of_proof (Symtab.update ((s, [(prop, prf')]), tab)) prf
        | Some ps => if exists (equal prop o fst) ps then tab else
            thms_of_proof (Symtab.update ((s, (prop, prf')::ps), tab)) prf)
+  | thms_of_proof tab (MinProof prfs) = foldl (uncurry thms_of_proof) (tab, prfs)
   | thms_of_proof tab _ = tab;
 
 fun axms_of_proof tab (Abst (_, _, prf)) = axms_of_proof tab prf
@@ -162,6 +163,7 @@
   | axms_of_proof tab (prf1 %% prf2) = axms_of_proof (axms_of_proof tab prf1) prf2
   | axms_of_proof tab (prf % _) = axms_of_proof tab prf
   | axms_of_proof tab (prf as PAxm (s, _, _)) = Symtab.update ((s, prf), tab)
+  | axms_of_proof tab (MinProof prfs) = foldl (uncurry axms_of_proof) (tab, prfs)
   | axms_of_proof tab _ = tab;
 
 (** collect all theorems, axioms and oracles **)