1.1 --- a/src/Tools/isac/MathEngBasic/istate.sml	Wed Nov 06 15:08:27 2019 +0100
     1.2 +++ b/src/Tools/isac/MathEngBasic/istate.sml	Wed Nov 06 18:34:29 2019 +0100
     1.3 @@ -25,14 +25,14 @@
     1.4    val trans_ass: pstate -> pstate -> pstate
     1.5    val trans_env_act: pstate -> pstate -> pstate
     1.6  
     1.7 -  val path_down: Celem.loc_ -> pstate -> pstate
     1.8 -  val path_down_form: (Celem.loc_ * term) -> pstate -> pstate
     1.9 -  val path_up': Celem.loc_ -> Celem.loc_
    1.10 +  val path_down: Celem.path -> pstate -> pstate
    1.11 +  val path_down_form: (Celem.path * term) -> pstate -> pstate
    1.12 +  val path_up': Celem.path -> Celem.path
    1.13    val path_up: pstate -> pstate
    1.14 -  val path_up_down: Celem.loc_ -> pstate -> pstate
    1.15 +  val path_up_down: Celem.path -> pstate -> pstate
    1.16  
    1.17    val upd_form: term -> pstate -> pstate
    1.18 -  val upd_path: Celem.loc_ -> pstate -> pstate
    1.19 +  val upd_path: Celem.path -> pstate -> pstate
    1.20    val upd_rls: Rule.rls -> pstate -> pstate
    1.21    val upd_act: term -> pstate -> pstate
    1.22    val upd_appy: appy_ -> pstate -> pstate
    1.23 @@ -82,7 +82,7 @@
    1.24  type pstate =  (* state for script interpreter                       *)
    1.25    {env: Env.T,(*stack*)  (* used to instantiate tac for checking associate
    1.26   	                12.03.noticed: e_ not updated during execution ?!? *)
    1.27 -  path: Celem.loc_,  (* location of tac in script                          *)
    1.28 +  path: Celem.path,  (* location of tac in script                          *)
    1.29    eval: Rule.rls,    (* for evaluating Prog_Expr                           *)
    1.30    form_arg:  term option, (*id FORMal ARGument of curried functions               *)
    1.31    act_arg: term,        (*vl ACTual ARGument (value) for execution of Tactic.T
    1.32 @@ -97,7 +97,7 @@
    1.33  fun topt2str NONE = "NONE"
    1.34    | topt2str (SOME t) = "SOME" ^ Rule.term2str t;
    1.35  fun scrstate2str {env, path, eval, form_arg, act_arg, or, finish, assoc} = (* for tests only *)
    1.36 -  "(" ^  Env.env2str env ^ ", " ^ Celem.loc_2str path ^ ", " ^ Rule.id_rls eval ^ ", " ^
    1.37 +  "(" ^  Env.env2str env ^ ", " ^ Celem.path2str path ^ ", " ^ Rule.id_rls eval ^ ", " ^
    1.38    topt2str form_arg ^ ", \n" ^ Rule.term2str act_arg ^ ", " ^ asap2str or ^ ", " ^
    1.39    appy_2str finish ^ ", " ^ bool2str assoc ^ ")";
    1.40