225 (*re-parse itms with a new thy and prepare for checking with ori list*) |
225 (*re-parse itms with a new thy and prepare for checking with ori list*) |
226 fun parsitm dI (itm as (i,v,b,f, Cor ((d,ts),_)):itm) = |
226 fun parsitm dI (itm as (i,v,b,f, Cor ((d,ts),_)):itm) = |
227 (* val itm as (i,v,b,f, Cor ((d,ts),_)) = hd probl; |
227 (* val itm as (i,v,b,f, Cor ((d,ts),_)) = hd probl; |
228 *) |
228 *) |
229 (let val t = (term_of o comp_dts (Isac "delay")) (d,ts); |
229 (let val t = (term_of o comp_dts (Isac "delay")) (d,ts); |
230 val s = Sign.string_of_term (sign_of dI) t; |
230 val s = Syntax.string_of_term (thy2ctxt dI) t; |
231 (*this ^ should raise the exn on unability of re-parsing dts*) |
231 (*this ^ should raise the exn on unability of re-parsing dts*) |
232 in itm end handle _ => ((i,v,false,f, Syn (term2str t)):itm)) |
232 in itm end handle _ => ((i,v,false,f, Syn (term2str t)):itm)) |
233 | parsitm dI (itm as (i,v,b,f, Syn str)) = |
233 | parsitm dI (itm as (i,v,b,f, Syn str)) = |
234 (let val t = (term_of o the o (parse dI)) str |
234 (let val t = (term_of o the o (parse dI)) str |
235 in (i,v,b,f, Par str) end handle _ => (i,v,b,f, Syn str)) |
235 in (i,v,b,f, Par str) end handle _ => (i,v,b,f, Syn str)) |
236 | parsitm dI (itm as (i,v,b,f, Typ str)) = |
236 | parsitm dI (itm as (i,v,b,f, Typ str)) = |
237 (let val t = (term_of o the o (parse dI)) str |
237 (let val t = (term_of o the o (parse dI)) str |
238 in (i,v,b,f, Par str) end handle _ => (i,v,b,f, Syn str)) |
238 in (i,v,b,f, Par str) end handle _ => (i,v,b,f, Syn str)) |
239 | parsitm dI (itm as (i,v,_,f, Inc ((d,ts),_))) = |
239 | parsitm dI (itm as (i,v,_,f, Inc ((d,ts),_))) = |
240 (let val t = (term_of o comp_dts (Isac "delay")) (d,ts); |
240 (let val t = (term_of o comp_dts (Isac "delay")) (d,ts); |
241 val s = Sign.string_of_term (sign_of dI) t; |
241 val s = Syntax.string_of_term (thy2ctxt dI) t; |
242 (*this ^ should raise the exn on unability of re-parsing dts*) |
242 (*this ^ should raise the exn on unability of re-parsing dts*) |
243 in itm end handle _ => ((i,v,false,f, Syn (term2str t)):itm)) |
243 in itm end handle _ => ((i,v,false,f, Syn (term2str t)):itm)) |
244 | parsitm dI (itm as (i,v,_,f, Sup (d,ts))) = |
244 | parsitm dI (itm as (i,v,_,f, Sup (d,ts))) = |
245 (let val t = (term_of o comp_dts (Isac"delay" )) (d,ts); |
245 (let val t = (term_of o comp_dts (Isac"delay" )) (d,ts); |
246 val s = Sign.string_of_term (sign_of dI) t; |
246 val s = Syntax.string_of_term (thy2ctxt dI) t; |
247 (*this ^ should raise the exn on unability of re-parsing dts*) |
247 (*this ^ should raise the exn on unability of re-parsing dts*) |
248 in itm end handle _ => ((i,v,false,f, Syn (term2str t)):itm)) |
248 in itm end handle _ => ((i,v,false,f, Syn (term2str t)):itm)) |
249 | parsitm dI (itm as (i,v,_,f, Mis (d,t'))) = |
249 | parsitm dI (itm as (i,v,_,f, Mis (d,t'))) = |
250 (let val t = d $ t'; |
250 (let val t = d $ t'; |
251 val s = Sign.string_of_term (sign_of dI) t; |
251 val s = Syntax.string_of_term (thy2ctxt dI) t; |
252 (*this ^ should raise the exn on unability of re-parsing dts*) |
252 (*this ^ should raise the exn on unability of re-parsing dts*) |
253 in itm end handle _ => ((i,v,false,f, Syn (term2str t)):itm)) |
253 in itm end handle _ => ((i,v,false,f, Syn (term2str t)):itm)) |
254 | parsitm dI (itm as (i,v,_,f, Par _)) = |
254 | parsitm dI (itm as (i,v,_,f, Par _)) = |
255 raise error ("parsitm ("^itm2str_ dI itm^ |
255 raise error ("parsitm ("^itm2str_ dI itm^ |
256 "): Par should be internal"); |
256 "): Par should be internal"); |