1.1 --- a/src/Tools/isac/MathEngBasic/istate.sml	Wed Oct 30 14:40:22 2019 +0100
     1.2 +++ b/src/Tools/isac/MathEngBasic/istate.sml	Wed Oct 30 16:46:05 2019 +0100
     1.3 @@ -25,6 +25,8 @@
     1.4    val get_subst: pstate -> (Env.T * (term option * term))
     1.5    val get_assoc: pstate -> bool
     1.6  
     1.7 +  val trans_scan_down2: pstate -> pstate
     1.8 +  val trans_scan_up2: pstate -> pstate
     1.9    val trans_ass: pstate -> pstate -> pstate
    1.10    val trans_env_act: pstate -> pstate -> pstate
    1.11  
    1.12 @@ -55,6 +57,8 @@
    1.13  struct
    1.14  (**)
    1.15  
    1.16 +open Celem
    1.17 +
    1.18  datatype appy_ = (* as argument in nxt_up, nstep_up, from appy               *)
    1.19  (*Appy              is only (final) returnvalue, not argument during search  *)
    1.20    AppUndef_
    1.21 @@ -115,6 +119,10 @@
    1.22  fun get_assoc (_, _, _, _, _, _, ass) = ass
    1.23  fun get_subst (env, _, _, form_arg, act_arg, _, _) = (env, (form_arg, act_arg))
    1.24  
    1.25 +fun trans_scan_down2 (env, _, rls, _, act_arg, _, _)  = 
    1.26 +  (env, [R], rls, NONE, act_arg, AppUndef_, false)
    1.27 +fun trans_scan_up2 (env, path, rls, form_arg, act_arg, _, _)  = 
    1.28 +  (env, path, rls, form_arg, act_arg, AppUndef_, false)
    1.29  fun trans_ass (_, _, _,  _,_, _, ass) (env, path, rls, form_arg, act_arg, safe, _) = 
    1.30    (env, path, rls, form_arg, act_arg, safe, ass)
    1.31  fun trans_env_act (env, _, _, _, act_arg, _, _) (_, path, rls, form_arg, _, safe, ass) =