136 ((lev_on p, Frm), (is, ctxt)))], c, (pt, pos))) |
136 ((lev_on p, Frm), (is, ctxt)))], c, (pt, pos))) |
137 end |
137 end |
138 | NONE => |
138 | NONE => |
139 let |
139 let |
140 val (m', (is', ctxt'), _) = (* re-design: should not be necessary *) |
140 val (m', (is', ctxt'), _) = (* re-design: should not be necessary *) |
141 LucinNEW.determine_next_tactic (pt, (p, Res)) sc (is, ctxt); |
141 LucinNEW.determine_next_tactic sc (pt, (p, Res)) is ctxt; |
142 in |
142 in |
143 case LucinNEW.locate_input_tactic sc (pt, (p, Res)) is' ctxt' m' of |
143 case LucinNEW.locate_input_tactic sc (pt, (p, Res)) is' ctxt' m' of |
144 LucinNEW.Safe_Step (istate, ctxt, tac) => |
144 LucinNEW.Safe_Step (istate, ctxt, tac) => |
145 let |
145 let |
146 val (p'', _, _,pt') = |
146 val (p'', _, _,pt') = |
175 Tactic.Check_elementwise _ => (*collects and instantiates asms*) |
175 Tactic.Check_elementwise _ => (*collects and instantiates asms*) |
176 (snd o (get_obj g_result pt)) p |
176 (snd o (get_obj g_result pt)) p |
177 | _ => get_assumptions_ pt (p,p_)) |
177 | _ => get_assumptions_ pt (p,p_)) |
178 handle _ => [] (*WN.27.5.03 asms in subpbls not completely clear*) |
178 handle _ => [] (*WN.27.5.03 asms in subpbls not completely clear*) |
179 val metID = get_obj g_metID pt pp; |
179 val metID = get_obj g_metID pt pp; |
180 val {srls = srls, scr = sc, ...} = Specify.get_met metID; |
180 val {scr = sc, ...} = Specify.get_met metID; |
181 val (loc, pst, ctxt) = case get_loc pt (p, p_) of |
181 val (pst, ctxt) = case get_loc pt (p, p_) of (Istate.Pstate pst, ctxt) => (pst, ctxt) |
182 loc as (Istate.Pstate pst, ctxt) => (loc, pst, ctxt) |
|
183 | _ => error "solve Check_Postcond: uncovered case get_loc" |
182 | _ => error "solve Check_Postcond: uncovered case get_loc" |
184 |
183 |
185 val thy' = get_obj g_domID pt pp; |
184 val thy' = get_obj g_domID pt pp; |
186 val thy = Celem.assoc_thy thy'; |
185 val thy = Celem.assoc_thy thy'; |
187 val (_, _, (scval, _(*scsaf*))) = LucinNEW.determine_next_tactic (pt, (p, p_)) sc loc; |
186 val (_, _, (scval, _(*scsaf*))) = LucinNEW.determine_next_tactic sc (pt, (p, p_)) (Istate.Pstate pst) ctxt; |
188 (* Telem.safe should go on to Check_Postcond' vvvvv *) |
187 (* Telem.safe should go on to Check_Postcond' vvvvv *) |
189 in |
188 in |
190 if pp = [] |
189 if pp = [] |
191 then |
190 then |
192 let |
191 let |