91 |
91 |
92 (*+*)val Rule_Set.Repeat {scr = EmptyProg, ...} = rls; (*this prog is replaced by Auto_Prog.gen on the fly*) |
92 (*+*)val Rule_Set.Repeat {scr = EmptyProg, ...} = rls; (*this prog is replaced by Auto_Prog.gen on the fly*) |
93 |
93 |
94 val tac_ = Tactic.Apply_Method' (Celem.e_metID(*WN0402: see generate1 !?!*), SOME t, is, ctxt) |
94 val tac_ = Tactic.Apply_Method' (Celem.e_metID(*WN0402: see generate1 !?!*), SOME t, is, ctxt) |
95 val pos' = ((lev_on o lev_dn) p, Frm) |
95 val pos' = ((lev_on o lev_dn) p, Frm) |
96 val thy = Celem.assoc_thy "Isac_Knowledge" |
96 val thy = ThyC.get_theory "Isac_Knowledge" |
97 val (_, _, _, pt') = Generate.generate1 tac_ (is, ctxt) (pt, pos') (* implicit Take *); |
97 val (_, _, _, pt') = Generate.generate1 tac_ (is, ctxt) (pt, pos') (* implicit Take *); |
98 |
98 |
99 (** )val (_,_, (pt'', _)) =( **) |
99 (** )val (_,_, (pt'', _)) =( **) |
100 complete_solve CompleteSubpbl [] (pt', pos'); |
100 complete_solve CompleteSubpbl [] (pt', pos'); |
101 "~~~~~ fun complete_solve , args:"; val (auto, c, (ptp as (_, p as (_, p_)))) |
101 "~~~~~ fun complete_solve , args:"; val (auto, c, (ptp as (_, p as (_, p_)))) |