278 hd (imodel2fstr imodel)); |
278 hd (imodel2fstr imodel)); |
279 *) |
279 *) |
280 fun appl_add' dI oris ppc pbt (sel, ct) = |
280 fun appl_add' dI oris ppc pbt (sel, ct) = |
281 let |
281 let |
282 val ctxt = assoc_thy dI |> thy2ctxt; |
282 val ctxt = assoc_thy dI |> thy2ctxt; |
283 in case parse (ProofContext.theory_of ctxt) ct of |
283 in case parseNEW ctxt ct of |
284 NONE => (0,[],false,sel, Syn ct):itm |
284 NONE => (0,[],false,sel, Syn ct):itm |
285 | SOME ct => (case is_known ctxt sel oris (term_of ct) of |
285 | SOME t => (case is_known ctxt sel oris t of |
286 ("", ori', all) => |
286 ("", ori', all) => |
287 (case is_notyet_input ctxt ppc all ori' pbt of |
287 (case is_notyet_input ctxt ppc all ori' pbt of |
288 ("",itm) => itm |
288 ("",itm) => itm |
289 | (msg,_) => error ("appl_add': " ^ msg)) |
289 | (msg,_) => error ("appl_add': " ^ msg)) |
290 | (_, (i, v, _, d, ts), _) => if is_e_ts ts then |
290 | (_, (i, v, _, d, ts), _) => if is_e_ts ts then |