57 (snd o (get_obj g_result pt)) p |
57 (snd o (get_obj g_result pt)) p |
58 | _ => get_assumptions_ pt (p,p_)) |
58 | _ => get_assumptions_ pt (p,p_)) |
59 handle _ => [] (*FIXME.WN030527 asms in subpbls not completely clear*) |
59 handle _ => [] (*FIXME.WN030527 asms in subpbls not completely clear*) |
60 val metID = get_obj g_metID pt pp; |
60 val metID = get_obj g_metID pt pp; |
61 val {srls=srls,scr=sc,...} = get_met metID; |
61 val {srls=srls,scr=sc,...} = get_met metID; |
62 val loc as (Pstate (E,l,a,_,_,b), ctxt) = get_loc pt (p,p_); |
62 val loc as (Pstate (E,l,rls,a,_,_,b), ctxt) = get_loc pt (p,p_); |
63 val thy' = get_obj g_domID pt pp; |
63 val thy' = get_obj g_domID pt pp; |
64 val thy = assoc_thy thy'; |
64 val thy = assoc_thy thy'; |
65 val (_,_,(scval,scsaf)) = determine_next_tactic (thy',srls) (pt,(p,p_)) sc loc; |
65 val (_,_,(scval,scsaf)) = determine_next_tactic (thy',srls) (pt,(p,p_)) sc loc; |
66 ;pp = []; (*false*) |
66 ;pp = []; (*false*) |
67 val ppp = par_pblobj pt (lev_up p); |
67 val ppp = par_pblobj pt (lev_up p); |
68 val thy' = get_obj g_domID pt ppp; |
68 val thy' = get_obj g_domID pt ppp; |
69 val thy = assoc_thy thy'; |
69 val thy = assoc_thy thy'; |
70 val metID = get_obj g_metID pt ppp; |
70 val metID = get_obj g_metID pt ppp; |
71 val {scr,...} = get_met metID; |
71 val {scr,...} = get_met metID; |
72 val (Pstate (E,l,a,_,_,b), ctxt') = get_loc pt (pp(*!/p/*),Frm) |
72 val (Pstate (E,l,rls,a,_,_,b), ctxt') = get_loc pt (pp(*!/p/*),Frm) |
73 val ctxt'' = from_subpbl_to_caller ctxt scval ctxt' |
73 val ctxt'' = from_subpbl_to_caller ctxt scval ctxt' |
74 val tac_ = Check_Postcond' (pI, (scval, asm)) |
74 val tac_ = Check_Postcond' (pI, (scval, asm)) |
75 val is = Pstate (E,l,a,scval,Istate.Skip_,b); |
75 val is = Pstate (E,l,rls,a,scval,Istate.Skip_,b); |
76 "~~~~~ fun generate1, args:"; val (thy, (Check_Postcond' (pI, (scval, asm))), l, (p,p_), pt) = |
76 "~~~~~ fun generate1, args:"; val (thy, (Check_Postcond' (pI, (scval, asm))), l, (p,p_), pt) = |
77 (thy, tac_, (is, ctxt''), (pp, Res), pt); |
77 (thy, tac_, (is, ctxt''), (pp, Res), pt); |
78 val (pt,c) = append_result pt p l (scval, (*map str2term*) asm) Complete; |
78 val (pt,c) = append_result pt p l (scval, (*map str2term*) asm) Complete; |
79 (*----------------------------------------############### changed*) |
79 (*----------------------------------------############### changed*) |
80 |
80 |