src/Pure/Proof/proof_syntax.ML
changeset 70418 d23cfb85438a
parent 70417 eb6ff14767cd
child 70443 a21a96eda033
equal deleted inserted replaced
70417:eb6ff14767cd 70418:d23cfb85438a
   127               | _ $ Const ("Pure.dummy_pattern", _) => NONE
   127               | _ $ Const ("Pure.dummy_pattern", _) => NONE
   128               | _ => SOME (mk_term t),
   128               | _ => SOME (mk_term t),
   129             Proofterm.incr_pboundvars 0 (~1) (prf_of [] prf))
   129             Proofterm.incr_pboundvars 0 (~1) (prf_of [] prf))
   130       | prf_of [] (Const ("Pure.AppP", _) $ prf1 $ prf2) =
   130       | prf_of [] (Const ("Pure.AppP", _) $ prf1 $ prf2) =
   131           prf_of [] prf1 %% prf_of [] prf2
   131           prf_of [] prf1 %% prf_of [] prf2
   132       | prf_of Ts (Const ("Pure.Appt", _) $ prf $ Const ("Pure.type", Type (_, [T]))) =
   132       | prf_of Ts (Const ("Pure.Appt", _) $ prf $ Const ("Pure.type", Type ("itself", [T]))) =
   133           prf_of (T::Ts) prf
   133           prf_of (T::Ts) prf
   134       | prf_of [] (Const ("Pure.Appt", _) $ prf $ t) = prf_of [] prf %
   134       | prf_of [] (Const ("Pure.Appt", _) $ prf $ t) = prf_of [] prf %
   135           (case t of Const ("Pure.dummy_pattern", _) => NONE | _ => SOME (mk_term t))
   135           (case t of Const ("Pure.dummy_pattern", _) => NONE | _ => SOME (mk_term t))
   136       | prf_of _ t = error ("Not a proof term:\n" ^
   136       | prf_of _ t = error ("Not a proof term:\n" ^
   137           Syntax.string_of_term_global thy t)
   137           Syntax.string_of_term_global thy t)