175 val tac = get_obj g_tac pt p |
175 val tac = get_obj g_tac pt p |
176 val ctxt = get_ctxt pt pos |
176 val ctxt = get_ctxt pt pos |
177 val rls = ((get_rls ctxt) o rls_of) tac |
177 val rls = ((get_rls ctxt) o rls_of) tac |
178 val ctxt = get_ctxt pt pos |
178 val ctxt = get_ctxt pt pos |
179 (*rls = Rule_Set.Repeat {calc = [], asm_rls = ...*) |
179 (*rls = Rule_Set.Repeat {calc = [], asm_rls = ...*) |
180 val is = Istate.init_detail tac t |
180 val is = Istate.init_detail ctxt tac t |
181 (*TODO.WN060602 Pstate (["(t_, Problem (Isac,[equation,univar]))"] |
181 (*TODO.WN060602 Pstate (["(t_, Problem (Isac,[equation,univar]))"] |
182 is wrong for simpl, but working ?!? *) |
182 is wrong for simpl, but working ?!? *) |
183 val tac_ = Apply_Method' (MethodC.id_empty(*WN0402: see Step.add !?!*), SOME t, is, ctxt) |
183 val tac_ = Apply_Method' (MethodC.id_empty(*WN0402: see Step.add !?!*), SOME t, is, ctxt) |
184 val pos' = ((lev_on o lev_dn) p, Frm) |
184 val pos' = ((lev_on o lev_dn) p, Frm) |
185 val thy = ThyC.get_theory "Isac_Knowledge" |
185 val thy = ThyC.get_theory "Isac_Knowledge" |