60 {scr = Rule.Prog sc, srls, erls, rew_ord' = ro, ...} => (sc, srls, erls, ro) |
60 {scr = Rule.Prog sc, srls, erls, rew_ord' = ro, ...} => (sc, srls, erls, ro) |
61 | _ => raise ERROR "specific_from_prog 1") |
61 | _ => raise ERROR "specific_from_prog 1") |
62 val (env, (a, v)) = (case get_istate_LI pt (p, p_) of |
62 val (env, (a, v)) = (case get_istate_LI pt (p, p_) of |
63 Istate.Pstate pst => (Istate.get_subst pst) | _ => error "specific_from_prog 2") |
63 Istate.Pstate pst => (Istate.get_subst pst) | _ => error "specific_from_prog 2") |
64 val ctxt = get_ctxt pt (p, p_) |
64 val ctxt = get_ctxt pt (p, p_) |
65 val alltacs = (*we expect at least 1 stac in a script*) |
65 val alltacs = (*we expect at least 1 Prog_Tac in a program*) |
66 map ((LItool.tac_from_prog pt thy) o Program.rep_stacexpr o #1 o |
66 map ((LItool.tac_from_prog pt thy) o Program.rep_stacexpr o #1 o |
67 (LItool.check_leaf "selrul" ctxt srls (env, (a, v)))) (Auto_Prog.stacpbls sc) |
67 (LItool.check_leaf "selrul" ctxt srls (env, (a, v)))) (Auto_Prog.stacpbls sc) |
68 val f = |
68 val f = |
69 (case p_ of Frm => get_obj g_form pt p | Res => (fst o (get_obj g_result pt)) p |
69 (case p_ of Frm => get_obj g_form pt p | Res => (fst o (get_obj g_result pt)) p |
70 | _ => raise ERROR "specific_from_prog 2") |
70 | _ => raise ERROR "specific_from_prog 2") |
71 (*WN071231 ? replace atomic_appl_tacs with applicable_in (ineff!) ?*) |
71 (*WN071231 ? replace atomic_appl_tacs with applicable_in (ineff!) ?*) |
72 in ((gen_distinct Tactic.eq_tac) o flat o (map (Rtools.atomic_appl_tacs thy ro erls f))) alltacs end; |
72 in |
|
73 ((gen_distinct Tactic.eq_tac) o flat o (map (Tactic.applicable thy ro erls f))) alltacs |
|
74 end; |
73 |
75 |
74 (**)end(**) |
76 (**)end(**) |