src/Pure/proofterm.ML

   | thms_of_proof tab (prf' as PThm ((s, _), prf, prop, _)) =
       (case Symtab.lookup (tab, s) of
          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
   | axms_of_proof tab (AbsP (_, _, prf)) = axms_of_proof tab prf
   | 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 **)
 
 fun mk_min_proof (prfs, Abst (_, _, prf)) = mk_min_proof (prfs, prf)