499 |
499 |
500 datatype input_term_result = Found_Step of Calc.T | Not_Derivable |
500 datatype input_term_result = Found_Step of Calc.T | Not_Derivable |
501 |
501 |
502 fun by_tactic (Tactic.Apply_Method' (mI, _, _, _)) (_, ctxt) (pt, pos as (p, _)) = |
502 fun by_tactic (Tactic.Apply_Method' (mI, _, _, _)) (_, ctxt) (pt, pos as (p, _)) = |
503 let |
503 let |
504 val (itms, oris, probl) = case get_obj I pt p of |
504 (*new*)val (itms, oris, probl) = case get_obj I pt p of |
505 PblObj {meth = itms, origin = (oris, _, _), probl, ...} => (itms, oris, probl) |
505 PblObj {meth = itms, origin = (oris, _, _), probl, ...} => (itms, oris, probl) |
506 | _ => raise ERROR "LI.by_tactic Apply_Method': uncovered case get_obj" |
506 | _ => raise ERROR "LI.by_tactic Apply_Method': uncovered case get_obj" |
507 val {model, ...} = MethodC.from_store ctxt mI; |
507 (*new*)val {model, ...} = MethodC.from_store ctxt mI; |
508 val itms = if itms <> [] then itms else I_Model.complete oris probl [] model |
508 val itms = if itms <> [] then itms else I_Model.complete oris probl [] model |
509 val (is, env, ctxt, prog) = case LItool.init_pstate ctxt (I_Model.OLD_to_TEST itms) mI of |
509 val (is, env, ctxt, prog) = case LItool.init_pstate ctxt (I_Model.OLD_to_TEST itms) mI of |
510 (is as Pstate {env, ...}, ctxt, program) => (is, env, ctxt, program) |
510 (is as Pstate {env, ...}, ctxt, program) => (is, env, ctxt, program) |
511 | _ => raise ERROR "LI.by_tactic Apply_Method': uncovered case init_pstate" |
511 | _ => raise ERROR "LI.by_tactic Apply_Method': uncovered case init_pstate" |
512 val ini = LItool.implicit_take ctxt prog env; |
512 val ini = LItool.implicit_take ctxt prog env; |