1.1 --- a/test/Tools/isac/MathEngine/mathengine-stateless.sml	Wed Oct 30 16:46:05 2019 +0100
     1.2 +++ b/test/Tools/isac/MathEngine/mathengine-stateless.sml	Thu Oct 31 10:41:42 2019 +0100
     1.3 @@ -487,9 +487,10 @@
     1.4  	        val (srls, is, sc) = from_pblobj_or_detail' thy' (p,p_) pt;
     1.5  	        val (tac_,is,(t,_)) = determine_next_tactic (thy',srls) (pt,pos) sc is;
     1.6  (*tac_ = Rewrite' (..., ("rnorm_equation_add", "Test.rnorm_equation_add"), ...) !!!!!!!!!!!!!!!!*)
     1.7 +
     1.8 +(*----- outcommented during cleanup of args in lucas-interpreter.sml ------------------------\\* )
     1.9  "~~~~~ fun determine_next_tactic , args:"; val (thy, (ptp as (pt, pos as (p, _)):ctree * pos'), 
    1.10    (sc as Prog (h $ body)), (Pstate (ist as (E,l,rls,a,v,s,b)), ctxt)) = ((thy',srls), (pt,pos), sc, is);
    1.11 -(*----- outcommented during cleanup of args in lucas-interpreter.sml ------------------------\\* )
    1.12  l = [] = false;
    1.13  nstep_up thy ptp sc ist Skip_ (*--> Appy (Rewrite' (.., (.., "Test.rnorm_equation_add"), ...)
    1.14    BUT WE FIND IN THE CODE ABOVE IN determine_next_tactic:*)