# HG changeset patch # User wenzelm # Date 1563788404 -7200 # Node ID 893d6373b484b34cfc81300466f5b4adf5ed2dd7 # Parent 9e53a98702b9d20f177a1acbab2bd561e26cd7f2 tuned; diff -r 9e53a98702b9 -r 893d6373b484 src/Pure/proofterm.ML --- a/src/Pure/proofterm.ML Mon Jul 22 11:39:30 2019 +0200 +++ b/src/Pure/proofterm.ML Mon Jul 22 11:40:04 2019 +0200 @@ -797,10 +797,10 @@ val t = the_default Term.dummy opt; val T = fastype_of1 (Ts, t) handle TERM _ => dummyT; in Const ("Pure.Appt", proofT --> T --> proofT) $ term_of Ts prf $ t end - | term_of Ts (Hyp t) = Hypt $ t - | term_of Ts (Oracle (_, t, _)) = Oraclet $ t - | term_of Ts MinProof = MinProoft - | term_of Ts (Promise (_, t, _)) = raise TERM ("Illegal proof promise", [t]); + | term_of _ (Hyp t) = Hypt $ t + | term_of _ (Oracle (_, t, _)) = Oraclet $ t + | term_of _ MinProof = MinProoft + | term_of _ (Promise (_, t, _)) = raise TERM ("Illegal proof promise", [t]); in