477 | generate1 thy (Subproblem' ((domID, pblID, metID), oris, hdl, fmz_, ctxt, f)) |
477 | generate1 thy (Subproblem' ((domID, pblID, metID), oris, hdl, fmz_, ctxt, f)) |
478 l (p,p_) pt = |
478 l (p,p_) pt = |
479 let (*val _=tracing("###generate1 Subproblem': pos= "^pos'2str (p,p_))*) |
479 let (*val _=tracing("###generate1 Subproblem': pos= "^pos'2str (p,p_))*) |
480 val (pt,c) = |
480 val (pt,c) = |
481 cappend_problem pt p l (fmz_, (domID, pblID, metID)) (oris, (domID, pblID, metID), hdl); |
481 cappend_problem pt p l (fmz_, (domID, pblID, metID)) (oris, (domID, pblID, metID), hdl); |
482 val pt = update_ctxt pt (p, Res) ctxt (*FIXME.WN110511*) |
482 val pt = update_pbl_ctxt pt p ctxt (*FIXME.WN110511*) |
483 val f = Syntax.string_of_term (thy2ctxt thy) f; |
483 val f = Syntax.string_of_term (thy2ctxt thy) f; |
484 in ((p,Pbl), c, Form' (FormKF (~1,EdUndef,(length p), Nundef, f)), pt) end |
484 in ((p,Pbl), c, Form' (FormKF (~1,EdUndef,(length p), Nundef, f)), pt) end |
485 |
485 |
486 | generate1 thy m' _ _ _ = |
486 | generate1 thy m' _ _ _ = |
487 error ("generate1: not impl.for "^(tac_2str m')) |
487 error ("generate1: not impl.for "^(tac_2str m')) |