151 val form = Ctree.get_obj Ctree.g_form pt p |
151 val form = Ctree.get_obj Ctree.g_form pt p |
152 (*val p = lev_on p; ---------------only difference to (..,Res) below*) |
152 (*val p = lev_on p; ---------------only difference to (..,Res) below*) |
153 val tacis = (Tactic.Begin_Trans, Tactic.Begin_Trans' form, (pos, (Istate_Def.Uistate, ctxt))) :: |
153 val tacis = (Tactic.Begin_Trans, Tactic.Begin_Trans' form, (pos, (Istate_Def.Uistate, ctxt))) :: |
154 (State_Steps.insert_pos ((Pos.lev_on o Pos.lev_dn) p) tacis) @ [(Tactic.End_Trans, Tactic.End_Trans' (res, asm), |
154 (State_Steps.insert_pos ((Pos.lev_on o Pos.lev_dn) p) tacis) @ [(Tactic.End_Trans, Tactic.End_Trans' (res, asm), |
155 (Pos.pos_plus (length tacis) (Pos.lev_dn p, Pos.Res), (Ctree.new_val res ist, ctxt)))] |
155 (Pos.pos_plus (length tacis) (Pos.lev_dn p, Pos.Res), (Ctree.new_val res ist, ctxt)))] |
156 val {nrls, ...} = Method.from_store (Ctree.get_obj Ctree.g_metID pt (Ctree.par_pblobj pt p)) |
156 val {nrls, ...} = MethodC.from_store (Ctree.get_obj Ctree.g_metID pt (Ctree.par_pblobj pt p)) |
157 val (pt, c, pos as (p, _)) = Solve_Step.s_add_general (rev tacis) (pt, [], (p, Pos.Res)) |
157 val (pt, c, pos as (p, _)) = Solve_Step.s_add_general (rev tacis) (pt, [], (p, Pos.Res)) |
158 val pt = Ctree.update_tac pt p (Tactic.Derive (Rule_Set.id nrls)) |
158 val pt = Ctree.update_tac pt p (Tactic.Derive (Rule_Set.id nrls)) |
159 val pt = Ctree.update_branch pt p Ctree.TransitiveB |
159 val pt = Ctree.update_branch pt p Ctree.TransitiveB |
160 in (c, (pt, pos)) end |
160 in (c, (pt, pos)) end |
161 | embed tacis (pt, (p, Pos.Res)) = |
161 | embed tacis (pt, (p, Pos.Res)) = |
169 val (f, _) = Ctree.get_obj Ctree.g_result pt p |
169 val (f, _) = Ctree.get_obj Ctree.g_result pt p |
170 val p = Pos.lev_on p(*---------------only difference to (..,Frm) above*); |
170 val p = Pos.lev_on p(*---------------only difference to (..,Frm) above*); |
171 val tacis = (Tactic.Begin_Trans, Tactic.Begin_Trans' f, ((p, Pos.Frm), (Istate_Def.Uistate, ctxt))) :: |
171 val tacis = (Tactic.Begin_Trans, Tactic.Begin_Trans' f, ((p, Pos.Frm), (Istate_Def.Uistate, ctxt))) :: |
172 (State_Steps.insert_pos ((Pos.lev_on o Pos.lev_dn) p) tacis) @ [(Tactic.End_Trans, Tactic.End_Trans' (res, asm), |
172 (State_Steps.insert_pos ((Pos.lev_on o Pos.lev_dn) p) tacis) @ [(Tactic.End_Trans, Tactic.End_Trans' (res, asm), |
173 (Pos.pos_plus (length tacis) (Pos.lev_dn p, Pos.Res), (Ctree.new_val res ist, ctxt)))]; |
173 (Pos.pos_plus (length tacis) (Pos.lev_dn p, Pos.Res), (Ctree.new_val res ist, ctxt)))]; |
174 val {nrls, ...} = Method.from_store (Ctree.get_obj Ctree.g_metID pt (Ctree.par_pblobj pt p)) |
174 val {nrls, ...} = MethodC.from_store (Ctree.get_obj Ctree.g_metID pt (Ctree.par_pblobj pt p)) |
175 val (pt, c, pos as (p, _)) = Solve_Step.s_add_general (rev tacis) (pt, [], (p, Pos.Res)) |
175 val (pt, c, pos as (p, _)) = Solve_Step.s_add_general (rev tacis) (pt, [], (p, Pos.Res)) |
176 val pt = Ctree.update_tac pt p (Tactic.Derive (Rule_Set.id nrls)) |
176 val pt = Ctree.update_tac pt p (Tactic.Derive (Rule_Set.id nrls)) |
177 val pt = Ctree.update_branch pt p Ctree.TransitiveB |
177 val pt = Ctree.update_branch pt p Ctree.TransitiveB |
178 in (c, (pt, pos)) end |
178 in (c, (pt, pos)) end |
179 | embed _ _ = raise ERROR "Derive.embed: uncovered definition" |
179 | embed _ _ = raise ERROR "Derive.embed: uncovered definition" |