1.1 --- a/test/Tools/isac/Minisubpbl/530-error-Check_Elementwise.sml	Wed Jan 15 12:01:13 2020 +0100
     1.2 +++ b/test/Tools/isac/Minisubpbl/530-error-Check_Elementwise.sml	Wed Jan 15 12:12:44 2020 +0100
     1.3 @@ -63,26 +63,26 @@
     1.4    = (sc, (pt, pos), ist, ctxt);
     1.5  
     1.6        (*case*)
     1.7 -           scan_to_tactic2 (prog, (ptp, ctxt)) (Istate.Pstate ist) (*of*);
     1.8 -"~~~~~ fun scan_to_tactic2 , args:"; val ((prog, cct), (Istate.Pstate (ist as {path, ...})))
     1.9 +           scan_to_tactic (prog, (ptp, ctxt)) (Istate.Pstate ist) (*of*);
    1.10 +"~~~~~ fun scan_to_tactic , args:"; val ((prog, cct), (Istate.Pstate (ist as {path, ...})))
    1.11    = ((prog, (ptp, ctxt)), (Istate.Pstate ist));
    1.12    (*if*) 0 = length path (*else*);
    1.13  
    1.14 -       go_scan_up2 (prog, cct) (trans_scan_up2 ist |> set_appy Skip_);
    1.15 -"~~~~~ and go_scan_up2 , args:"; val ((yyy as (prog, _)), (ist as {env, path, finish, ...}))
    1.16 +       go_scan_up (prog, cct) (trans_scan_up2 ist |> set_appy Skip_);
    1.17 +"~~~~~ and go_scan_up , args:"; val ((yyy as (prog, _)), (ist as {env, path, finish, ...}))
    1.18    = ((prog, cct), (trans_scan_up2 ist |> set_appy Skip_));
    1.19      (*if*) 1 < length path (*then*);
    1.20  
    1.21 -           scan_up2 yyy (ist |> path_up) (go_up path prog);
    1.22 -"~~~~~ fun scan_up2 , args:"; val ((yyy as (prog, xxx)), (ist as {finish, ...}), (Const ("HOL.Let"(*1*), _) $ _))
    1.23 +           scan_up yyy (ist |> path_up) (go_up path prog);
    1.24 +"~~~~~ fun scan_up , args:"; val ((yyy as (prog, xxx)), (ist as {finish, ...}), (Const ("HOL.Let"(*1*), _) $ _))
    1.25    = (yyy, (ist |> path_up), (go_up path prog));
    1.26      (*if*) finish = Napp_ (*else*);
    1.27          val (i, body) = check_Let_up ist prog;
    1.28  
    1.29          (*case*)
    1.30 -           scan_dn2 xxx (ist |> path_up_down [R, D] |> upd_env i) body (*of*);
    1.31 +           scan_dn xxx (ist |> path_up_down [R, D] |> upd_env i) body (*of*);
    1.32      (*========== a leaf has been found ==========*)   
    1.33 -"~~~~~ fun scan_dn2 , args:"; val (((pt, p), ctxt), (ist as {env, eval, ...}), t)
    1.34 +"~~~~~ fun scan_dn , args:"; val (((pt, p), ctxt), (ist as {env, eval, ...}), t)
    1.35    = (xxx, (ist |> path_up_down [R, D] |> upd_env i), body);
    1.36    val (Program.Tac stac, a') = (*case*)
    1.37        interpret_leaf "next " ctxt eval (get_subst ist) t;