110 val _(*f_pred*) = Ctree.get_curr_formula (pt, pos_pred); |
110 val _(*f_pred*) = Ctree.get_curr_formula (pt, pos_pred); |
111 |
111 |
112 (*case*) compare_step ([], [], (pt, pos_pred)) tm (*of*); |
112 (*case*) compare_step ([], [], (pt, pos_pred)) tm (*of*); |
113 "~~~~~ fun compare_step , args:"; val ((tacis, c, ptp as (pt, pos as (p, _))), ifo) = (([], [], (pt, pos_pred)), tm); |
113 "~~~~~ fun compare_step , args:"; val ((tacis, c, ptp as (pt, pos as (p, _))), ifo) = (([], [], (pt, pos_pred)), tm); |
114 val fo = Calc.current_formula ptp |
114 val fo = Calc.current_formula ptp |
115 val {nrls, ...} = Specify.get_met (Ctree.get_obj Ctree.g_metID pt (Ctree.par_pblobj pt p)) |
115 val {nrls, ...} = Method.from_store (Ctree.get_obj Ctree.g_metID pt (Ctree.par_pblobj pt p)) |
116 val {rew_ord, erls, rules, ...} = Rule_Set.rep nrls |
116 val {rew_ord, erls, rules, ...} = Rule_Set.rep nrls |
117 val (found, der) = Derive.steps rew_ord erls rules fo ifo; (*<---------------*) |
117 val (found, der) = Derive.steps rew_ord erls rules fo ifo; (*<---------------*) |
118 (*if*) found (*then*); |
118 (*if*) found (*then*); |
119 val tacis' = map (State_Steps.make_single rew_ord erls) der; |
119 val tacis' = map (State_Steps.make_single rew_ord erls) der; |
120 |
120 |
128 val (f, _) = Ctree.get_obj Ctree.g_result pt p |
128 val (f, _) = Ctree.get_obj Ctree.g_result pt p |
129 val p = Pos.lev_on p(*---------------only difference to (..,Frm) above*); |
129 val p = Pos.lev_on p(*---------------only difference to (..,Frm) above*); |
130 val tacis = (Tactic.Begin_Trans, Tactic.Begin_Trans' f, ((p, Pos.Frm), (Istate_Def.Uistate, ctxt))) :: |
130 val tacis = (Tactic.Begin_Trans, Tactic.Begin_Trans' f, ((p, Pos.Frm), (Istate_Def.Uistate, ctxt))) :: |
131 (State_Steps.insert_pos ((Pos.lev_on o Pos.lev_dn) p) tacis) @ [(Tactic.End_Trans, Tactic.End_Trans' (res, asm), |
131 (State_Steps.insert_pos ((Pos.lev_on o Pos.lev_dn) p) tacis) @ [(Tactic.End_Trans, Tactic.End_Trans' (res, asm), |
132 (Pos.pos_plus (length tacis) (Pos.lev_dn p, Pos.Res), (Ctree.new_val res ist, ctxt)))]; |
132 (Pos.pos_plus (length tacis) (Pos.lev_dn p, Pos.Res), (Ctree.new_val res ist, ctxt)))]; |
133 val {nrls, ...} = Specify.get_met (Ctree.get_obj Ctree.g_metID pt (Ctree.par_pblobj pt p)) |
133 val {nrls, ...} = Method.from_store (Ctree.get_obj Ctree.g_metID pt (Ctree.par_pblobj pt p)) |
134 val (pt, c, pos as (p, _)) = |
134 val (pt, c, pos as (p, _)) = |
135 |
135 |
136 Solve_Step.s_add_general (rev tacis) (pt, [], (p, Res)); |
136 Solve_Step.s_add_general (rev tacis) (pt, [], (p, Res)); |
137 "~~~~~ fun s_add_general , args:"; val (tacis, (pt, c, _)) = ((rev tacis), (pt, [], (p, Res))); |
137 "~~~~~ fun s_add_general , args:"; val (tacis, (pt, c, _)) = ((rev tacis), (pt, [], (p, Res))); |
138 (*+*)length tacis = 8; |
138 (*+*)length tacis = 8; |