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 (ScrState (E,l,a,_,_,b), ctxt') = get_loc pt (pp(*!/p/*),Frm) |
72 val (ScrState (E,l,a,_,_,b), ctxt') = get_loc pt (pp(*!/p/*),Frm) |
73 val ctxt'' = transfer_from_subproblem ctxt 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 = ScrState (E,l,a,scval,scsaf,b); |
75 val is = ScrState (E,l,a,scval,scsaf,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; |