131 | _ $ Const ("Pure.dummy_pattern", _) => NONE |
131 | _ $ Const ("Pure.dummy_pattern", _) => NONE |
132 | _ => SOME (mk_term t), |
132 | _ => SOME (mk_term t), |
133 Proofterm.incr_pboundvars 0 (~1) (prf_of [] prf)) |
133 Proofterm.incr_pboundvars 0 (~1) (prf_of [] prf)) |
134 | prf_of [] (Const ("AppP", _) $ prf1 $ prf2) = |
134 | prf_of [] (Const ("AppP", _) $ prf1 $ prf2) = |
135 prf_of [] prf1 %% prf_of [] prf2 |
135 prf_of [] prf1 %% prf_of [] prf2 |
136 | prf_of Ts (Const ("Appt", _) $ prf $ Const ("TYPE", Type (_, [T]))) = |
136 | prf_of Ts (Const ("Appt", _) $ prf $ Const ("Pure.type", Type (_, [T]))) = |
137 prf_of (T::Ts) prf |
137 prf_of (T::Ts) prf |
138 | prf_of [] (Const ("Appt", _) $ prf $ t) = prf_of [] prf % |
138 | prf_of [] (Const ("Appt", _) $ prf $ t) = prf_of [] prf % |
139 (case t of Const ("Pure.dummy_pattern", _) => NONE | _ => SOME (mk_term t)) |
139 (case t of Const ("Pure.dummy_pattern", _) => NONE | _ => SOME (mk_term t)) |
140 | prf_of _ t = error ("Not a proof term:\n" ^ |
140 | prf_of _ t = error ("Not a proof term:\n" ^ |
141 Syntax.string_of_term_global thy t) |
141 Syntax.string_of_term_global thy t) |