1.1 --- a/src/Tools/isac/Interpret/lucas-interpreter.sml	Thu Sep 29 18:02:10 2022 +0200
     1.2 +++ b/src/Tools/isac/Interpret/lucas-interpreter.sml	Fri Oct 07 20:46:48 2022 +0200
     1.3 @@ -498,8 +498,8 @@
     1.4  
     1.5  fun by_tactic (Tactic.Apply_Method' (mI, _, _, _)) (_, ctxt) (pt, pos as (p, _)) =
     1.6        let
     1.7 -         val (itms, oris, probl, ctxt) = case get_obj I pt p of
     1.8 -           PblObj {meth = itms, origin = (oris, _, _), probl, ctxt, ...} => (itms, oris, probl, ctxt)
     1.9 +         val (itms, oris, probl) = case get_obj I pt p of (*STILL asms=[]*)
    1.10 +           PblObj {meth = itms, origin = (oris, _, _), probl, ...} => (itms, oris, probl)
    1.11           | _ => raise ERROR "LI.by_tactic Apply_Method': uncovered case get_obj"
    1.12           val {ppc, ...} = MethodC.from_store_PIDE ctxt mI;
    1.13           val itms = if itms <> [] then itms else I_Model.complete oris probl [] ppc
    1.14 @@ -551,8 +551,8 @@
    1.15          val {scr, ...} = MethodC.from_store_PIDE ctxt (get_obj g_metID pt parent_pos);
    1.16          val prog_res =
    1.17             case find_next_step scr (pt, pos) sub_ist sub_ctxt of
    1.18 -  (*OLD*)    Next_Step (_, _, Tactic.Check_elementwise' (_, _, (prog_res, _))) => prog_res
    1.19 -    |(*OLD*) End_Program (_, Tactic.Check_Postcond' (_, prog_res)) => prog_res
    1.20 +             Next_Step (_, _, Tactic.Check_elementwise' (_, _, (prog_res, _))) => prog_res
    1.21 +           | End_Program (_, Tactic.Check_Postcond' (_, prog_res)) => prog_res
    1.22             | _ => raise ERROR ("Step_Solve.by_tactic Check_Postcond " ^ strs2str' pI)
    1.23        in
    1.24          if parent_pos = [] then