55 | make_single ctxt _ _ (t, r as Rule.Rls_ rls, (t', a)) = |
55 | make_single ctxt _ _ (t, r as Rule.Rls_ rls, (t', a)) = |
56 (Tactic.Rewrite_Set (Rule_Set.id_from_rule ctxt r), |
56 (Tactic.Rewrite_Set (Rule_Set.id_from_rule ctxt r), |
57 Tactic.Rewrite_Set' ("Isac_Knowledge", false, rls, t, (t', a)), |
57 Tactic.Rewrite_Set' ("Isac_Knowledge", false, rls, t, (t', a)), |
58 (Pos.e_pos'(*to be updated before generate tacis!!!*), (Istate_Def.Uistate, ContextC.empty))) |
58 (Pos.e_pos'(*to be updated before generate tacis!!!*), (Istate_Def.Uistate, ContextC.empty))) |
59 | make_single ctxt _ _ (t, r, _) = raise ERROR ("State_Steps.make_single: not impl. for " ^ |
59 | make_single ctxt _ _ (t, r, _) = raise ERROR ("State_Steps.make_single: not impl. for " ^ |
60 Rule.to_string_PIDE ctxt r ^ " at " ^ UnparseC.term_in_ctxt ctxt t) |
60 Rule.to_string ctxt r ^ " at " ^ UnparseC.term_in_ctxt ctxt t) |
61 |
61 |
62 (* update pos in tacis for embedding by generate *) |
62 (* update pos in tacis for embedding by generate *) |
63 fun insert_pos (_: Pos.pos) [] = [] |
63 fun insert_pos (_: Pos.pos) [] = [] |
64 | insert_pos (p: Pos.pos) (((tac, tac_, (_, ist)): single) :: tacis) = |
64 | insert_pos (p: Pos.pos) (((tac, tac_, (_, ist)): single) :: tacis) = |
65 ((tac, tac_, ((p, Pos.Res), ist)): single) :: (insert_pos (Pos.lev_on p) tacis) |
65 ((tac, tac_, ((p, Pos.Res), ist)): single) :: (insert_pos (Pos.lev_on p) tacis) |