1.1 --- a/src/Tools/isac/Interpret/istate.sml	Thu Aug 22 11:26:14 2019 +0200
     1.2 +++ b/src/Tools/isac/Interpret/istate.sml	Thu Aug 22 12:18:58 2019 +0200
     1.3 @@ -11,7 +11,7 @@
     1.4    val e_scrstate : scrstate
     1.5    val scrstate2str : Rule.subst * Celem.loc_ * term option * term * safe * bool -> string
     1.6  
     1.7 -  datatype T = RrlsState of Rule.rrlsstate | ScrState of scrstate | Uistate
     1.8 +  datatype T = RrlsState of Rule.rrlsstate | Pstate of scrstate | Uistate
     1.9    val istate2str : T -> string
    1.10    val istates2str : T option * T option -> string
    1.11    val e_istate : T
    1.12 @@ -48,14 +48,14 @@
    1.13  (* for handling type T see fun from_pblobj_or_detail', +? *)
    1.14  datatype T =                 (*interpreter state*)
    1.15  	  Uistate                       (*undefined in modspec, in '_deriv'ation*)
    1.16 -  | ScrState of scrstate          (*for script interpreter*)
    1.17 +  | Pstate of scrstate          (*for script interpreter*)
    1.18    | RrlsState of Rule.rrlsstate; (*for reverse rewriting*)
    1.19 -val e_istate = (ScrState ([], [], NONE, Rule.e_term, Sundef, false));
    1.20 +val e_istate = (Pstate ([], [], NONE, Rule.e_term, Sundef, false));
    1.21  
    1.22  fun rta2str (r, (t, a)) = "\n(" ^ Rule.rule2str r ^ ",(" ^ Rule.term2str t ^", " ^ Rule.terms2str a ^ "))";
    1.23  fun istate2str Uistate = "Uistate"
    1.24 -  | istate2str (ScrState (e, l, to, t, s, b)) =
    1.25 -    "ScrState ("^ Celem.subst2str e ^ ",\n " ^ 
    1.26 +  | istate2str (Pstate (e, l, to, t, s, b)) =
    1.27 +    "Pstate ("^ Celem.subst2str e ^ ",\n " ^ 
    1.28      Celem.loc_2str l ^ ", " ^ Rule.termopt2str to ^ ",\n " ^
    1.29      Rule.term2str t ^ ", " ^ safe2str s ^ ", " ^ bool2str b ^ ")"
    1.30    | istate2str (RrlsState (t, t1, rss, rtas)) =