476 (oris, (domID, pblID, metID), hdl); |
476 (oris, (domID, pblID, metID), hdl); |
477 (*val pbl = init_pbl ((#ppc o get_pbt) pblID); |
477 (*val pbl = init_pbl ((#ppc o get_pbt) pblID); |
478 val pt = update_pblppc pt p pbl;--------4.9.03->Model_Problem*) |
478 val pt = update_pblppc pt p pbl;--------4.9.03->Model_Problem*) |
479 (*val _= writeln("### generate1: is([3],Frm)= "^ |
479 (*val _= writeln("### generate1: is([3],Frm)= "^ |
480 (istate2str (get_istate pt ([3],Frm))));*) |
480 (istate2str (get_istate pt ([3],Frm))));*) |
481 val f = Sign.string_of_term (sign_of thy) f; |
481 val f = Syntax.string_of_term (thy2ctxt thy) f; |
482 in ((p,Pbl), c, Form' (FormKF (~1,EdUndef,(length p), Nundef, f)), pt) end |
482 in ((p,Pbl), c, Form' (FormKF (~1,EdUndef,(length p), Nundef, f)), pt) end |
483 |
483 |
484 | generate1 thy m' _ _ _ = |
484 | generate1 thy m' _ _ _ = |
485 raise error ("generate1: not impl.for "^(tac_2str m')) |
485 raise error ("generate1: not impl.for "^(tac_2str m')) |
486 ; |
486 ; |