--- a/src/Pure/Proof/proof_syntax.ML Fri Mar 21 12:14:33 2014 +0100
+++ b/src/Pure/Proof/proof_syntax.ML Fri Mar 21 12:34:50 2014 +0100
@@ -133,7 +133,7 @@
Proofterm.incr_pboundvars 0 (~1) (prf_of [] prf))
| prf_of [] (Const ("AppP", _) $ prf1 $ prf2) =
prf_of [] prf1 %% prf_of [] prf2
- | prf_of Ts (Const ("Appt", _) $ prf $ Const ("TYPE", Type (_, [T]))) =
+ | prf_of Ts (Const ("Appt", _) $ prf $ Const ("Pure.type", Type (_, [T]))) =
prf_of (T::Ts) prf
| prf_of [] (Const ("Appt", _) $ prf $ t) = prf_of [] prf %
(case t of Const ("Pure.dummy_pattern", _) => NONE | _ => SOME (mk_term t))