# HG changeset patch
# User wenzelm
# Date 1565878638 -7200
# Node ID de6062ac70b6d49f8bc601989548a6aa70b0c18c
# Parent  fb876ebbf5a711ef4c9a0fa27d0965038f49cd71
more complete pattern match;

diff -r fb876ebbf5a7 -r de6062ac70b6 src/Pure/term.scala
--- a/src/Pure/term.scala	Thu Aug 15 16:06:57 2019 +0200
+++ b/src/Pure/term.scala	Thu Aug 15 16:17:18 2019 +0200
@@ -157,7 +157,6 @@
           case Some(y) => y
           case None =>
             x match {
-              case MinProof => x
               case PBound(index) => store(PBound(cache_int(index)))
               case Abst(name, typ, body) =>
                 store(Abst(cache_string(name), cache_typ(typ), cache_proof(body)))
@@ -165,6 +164,8 @@
                 store(AbsP(cache_string(name), cache_term(hyp), cache_proof(body)))
               case Appt(fun, arg) => store(Appt(cache_proof(fun), cache_term(arg)))
               case AppP(fun, arg) => store(AppP(cache_proof(fun), cache_proof(arg)))
+              case Hyp(hyp) => store(Hyp(cache_term(hyp)))
+              case PAxm(name, types) => store(PAxm(cache_string(name), cache_typs(types)))
               case OfClass(typ, cls) => store(OfClass(cache_typ(typ), cache_string(cls)))
               case Oracle(name, prop, types) =>
                 store(Oracle(cache_string(name), cache_term(prop), cache_typs(types)))