219 Ctree.PblObj {fmz = fmz as (fmz_,_), origin = (oris, ospec, hdf'), |
219 Ctree.PblObj {fmz = fmz as (fmz_,_), origin = (oris, ospec, hdf'), |
220 spec = sspec as (sdI, spI, smI), probl, meth, ...} |
220 spec = sspec as (sdI, spI, smI), probl, meth, ...} |
221 => (fmz, fmz_, oris, ospec, hdf', sspec, sdI, spI, smI, probl, meth) |
221 => (fmz, fmz_, oris, ospec, hdf', sspec, sdI, spI, smI, probl, meth) |
222 | _ => raise ERROR "input_icalhd: uncovered case of get_obj I pt p" |
222 | _ => raise ERROR "input_icalhd: uncovered case of get_obj I pt p" |
223 val ctxt = Proof_Context.init_global (ThyC.get_theory sdI) |
223 val ctxt = Proof_Context.init_global (ThyC.get_theory sdI) |
224 in if CAS_Cmd.is_from hdf fmz then the (CAS_Cmd.input (TermC.str2term hdf)) |
224 in if CAS_Cmd.is_from hdf fmz then the (CAS_Cmd.input (TermC.parse ctxt hdf)) |
225 else (*hacked WN0602 ~~~ ~~~~~~~~~, ..dropped !*) |
225 else (*hacked WN0602 ~~~ ~~~~~~~~~, ..dropped !*) |
226 let val (pos_, pits, mits) = |
226 let val (pos_, pits, mits) = |
227 if dI <> sdI |
227 if dI <> sdI |
228 then let val its = map (parsitm (ThyC.get_theory dI)) probl; |
228 then let val its = map (parsitm (ThyC.get_theory dI)) probl; |
229 val (its, trms) = filter_sep is_Par its; |
229 val (its, trms) = filter_sep is_Par its; |