385 val p = case p_ of |
385 val p = case p_ of |
386 Frm => p | Res => lev_on p |
386 Frm => p | Res => lev_on p |
387 | _ => error ("generate_hard: call by " ^ pos'2str (p,p_)) |
387 | _ => error ("generate_hard: call by " ^ pos'2str (p,p_)) |
388 in generate1 thy m' (Selem.e_istate, Selem.e_ctxt) (p,p_) pt end |
388 in generate1 thy m' (Selem.e_istate, Selem.e_ctxt) (p,p_) pt end |
389 |
389 |
390 (* tacis are in reverse order from nxt_solve_/specify_: last = fst to insert *) |
390 (* tacis are in reverse order from do_solve_step/specify_: last = fst to insert *) |
391 fun generate ([]: taci list) ptp = ptp |
391 fun generate ([]: taci list) ptp = ptp |
392 | generate tacis (pt, c, _: pos'(*!dropped!WN0504redesign generate/tacis?*))= |
392 | generate tacis (pt, c, _: pos'(*!dropped!WN0504redesign generate/tacis?*))= |
393 let |
393 let |
394 val (tacis', (_, tac_, (p, is))) = split_last tacis |
394 val (tacis', (_, tac_, (p, is))) = split_last tacis |
395 val (p',c',_,pt') = generate1 (Celem.assoc_thy "Isac") tac_ is p pt |
395 val (p',c',_,pt') = generate1 (Celem.assoc_thy "Isac") tac_ is p pt |