# HG changeset patch
# User wenzelm
# Date 1564147262 -7200
# Node ID d23cfb85438a38a55a0fe5ffd23bb98e7d6e4132
# Parent  eb6ff14767cd28679a7d2a899df47de628e3eb24
proper argument type (amending 42fbb6abed5a);

diff -r eb6ff14767cd -r d23cfb85438a src/Pure/Proof/proof_syntax.ML
--- a/src/Pure/Proof/proof_syntax.ML	Fri Jul 26 14:43:56 2019 +0200
+++ b/src/Pure/Proof/proof_syntax.ML	Fri Jul 26 15:21:02 2019 +0200
@@ -129,7 +129,7 @@
             Proofterm.incr_pboundvars 0 (~1) (prf_of [] prf))
       | prf_of [] (Const ("Pure.AppP", _) $ prf1 $ prf2) =
           prf_of [] prf1 %% prf_of [] prf2
-      | prf_of Ts (Const ("Pure.Appt", _) $ prf $ Const ("Pure.type", Type (_, [T]))) =
+      | prf_of Ts (Const ("Pure.Appt", _) $ prf $ Const ("Pure.type", Type ("itself", [T]))) =
           prf_of (T::Ts) prf
       | prf_of [] (Const ("Pure.Appt", _) $ prf $ t) = prf_of [] prf %
           (case t of Const ("Pure.dummy_pattern", _) => NONE | _ => SOME (mk_term t))