1.1 --- a/src/Tools/isac/Interpret/li-tool.sml	Wed Mar 18 14:51:58 2020 +0100
     1.2 +++ b/src/Tools/isac/Interpret/li-tool.sml	Wed Mar 18 15:23:15 2020 +0100
     1.3 @@ -17,8 +17,8 @@
     1.4  
     1.5    val get_simplifier : Calc.T -> Rule.rls
     1.6  (*vvv initialise : Rule.theory'(*?!?*) -> Calc.T -> (Istate.T * Proof.context) * Program.T*)
     1.7 -  val from_pblobj_or_detail' : Rule.theory' -> Ctree.pos' -> Ctree.ctree -> 
     1.8 -    Rule.rls(*..\<in> ist \<rightarrow> REMOVE*) * (Istate.T * Proof.context) * Program.T
     1.9 +  val resume_prog : Rule.theory' -> Ctree.pos' -> Ctree.ctree -> 
    1.10 +    (Istate.T * Proof.context) * Program.T
    1.11  
    1.12    val tac_from_prog : Ctree.ctree -> theory -> term -> Tactic.input
    1.13    val check_leaf : string -> Proof.context -> Rule.rls -> (Env.T * (term option * term)) -> term -> 
    1.14 @@ -346,23 +346,23 @@
    1.15  	  val {srls, ...} = Specify.get_met metID
    1.16    in srls end
    1.17  
    1.18 -(* decide, where to get program/istate from:
    1.19 +(* decide, where to get program/istate/ctxt from:
    1.20     (* 1 *) from PblObj: at begin of program if no init_form
    1.21     (* 2 *) from PblObj/PrfObj: if Prog_Tac is in the middle of the program
    1.22     (* 3 *) from PrfOb: in case of Math_Engine.detailstep
    1.23   *)
    1.24 -fun from_pblobj_or_detail' thy (p, p_) pt =
    1.25 +fun resume_prog thy (p, p_) pt =
    1.26    if Pos.on_specification p_
    1.27    then case get_obj g_env (*!DEPRECATED!*) pt p of                                         (* 1 *)
    1.28 -      NONE => error "from_pblobj_or_detail': no istate"
    1.29 +      NONE => error "resume_prog: no istate"
    1.30      | SOME (Istate.Pstate pst, ctxt) =>
    1.31          let
    1.32            val metID = get_obj g_metID pt p
    1.33            val {srls, ...} = Specify.get_met metID
    1.34          in
    1.35 -          (srls, (Istate.Pstate (Istate.set_eval srls pst), ctxt), (#scr o Specify.get_met) metID)
    1.36 +          ((Istate.Pstate (Istate.set_eval srls pst), ctxt), (#scr o Specify.get_met) metID)
    1.37          end
    1.38 -    | _ => raise ERROR "from_pblobj_or_detail': unexpected result from g_env"
    1.39 +    | _ => raise ERROR "resume_prog: unexpected result from g_env"
    1.40    else
    1.41      let val (pbl, p', rls') = par_pbl_det pt p
    1.42      in if pbl
    1.43 @@ -373,11 +373,10 @@
    1.44  	         val (is, ctxt) =
    1.45  	           case get_loc pt (p, p_) of
    1.46  	              (Istate.Pstate ist, ctxt) => (Istate.Pstate (Istate.set_eval srls ist), ctxt)
    1.47 -	           | _ => raise ERROR "from_pblobj_or_detail': unexpected result from get_loc"
    1.48 -	       in (srls, (is, ctxt), (#scr o Specify.get_met) metID) end
    1.49 +	           | _ => raise ERROR "resume_prog: unexpected result from get_loc"
    1.50 +	       in ((is, ctxt), (#scr o Specify.get_met) metID) end
    1.51         else                                                                                (* 3 *)
    1.52 -         (Rule.e_rls(*!!!*),
    1.53 -         get_loc pt (p, p_),
    1.54 +         (get_loc pt (p, p_),
    1.55           Rule.Prog (Auto_Prog.gen (Celem.assoc_thy thy) (get_last_formula (pt, (p, p_))) rls'))
    1.56      end
    1.57  

     2.1 --- a/src/Tools/isac/Interpret/lucas-interpreter.sml	Wed Mar 18 14:51:58 2020 +0100
     2.2 +++ b/src/Tools/isac/Interpret/lucas-interpreter.sml	Wed Mar 18 15:23:15 2020 +0100
     2.3 @@ -575,7 +575,7 @@
     2.4      else 
     2.5        let 
     2.6          val thy' = get_obj g_domID pt (par_pblobj pt p);
     2.7 -	      val (_, (ist, ctxt), sc) = LItool.from_pblobj_or_detail' thy' (p,p_) pt;
     2.8 +	      val ((ist, ctxt), sc) = LItool.resume_prog thy' (p,p_) pt;
     2.9        in
    2.10          case find_next_step sc (pt, pos) ist ctxt of
    2.11             Next_Step (ist, ctxt, tac) =>

     3.1 --- a/src/Tools/isac/Interpret/step-solve.sml	Wed Mar 18 14:51:58 2020 +0100
     3.2 +++ b/src/Tools/isac/Interpret/step-solve.sml	Wed Mar 18 15:23:15 2020 +0100
     3.3 @@ -104,7 +104,7 @@
     3.4      else
     3.5  	    let 
     3.6  	      val thy' = get_obj g_domID pt (par_pblobj pt p);
     3.7 -	      val (_, is, sc) = LItool.from_pblobj_or_detail' thy' (p,p_) pt;
     3.8 +	      val (is, sc) = LItool.resume_prog thy' (p,p_) pt;
     3.9  	    in
    3.10          case LI.locate_input_tactic sc (pt, po) (fst is) (snd is) m of
    3.11            LI.Safe_Step (istate, ctxt, tac) =>

     4.1 --- a/src/Tools/isac/MathEngBasic/istate-def.sml	Wed Mar 18 14:51:58 2020 +0100
     4.2 +++ b/src/Tools/isac/MathEngBasic/istate-def.sml	Wed Mar 18 15:23:15 2020 +0100
     4.3 @@ -67,7 +67,7 @@
     4.4    topt2str form_arg ^ ", " ^ Rule.term2str act_arg ^ ", " ^ asap2str or ^ ", " ^
     4.5    bool2str found_accept ^ ", " ^ bool2str assoc ^ ")";
     4.6  
     4.7 -(* for handling type T see fun from_pblobj_or_detail', +? *)
     4.8 +(* for handling type T see fun resume_prog, +? *)
     4.9  datatype T =                 (*interpreter state*)
    4.10  	  Uistate                       (*undefined in modspec, in '_deriv'ation*)
    4.11    | Pstate of pstate          (*for script interpreter*)

     5.1 --- a/src/Tools/isac/ProgLang/Auto_Prog.thy	Wed Mar 18 14:51:58 2020 +0100
     5.2 +++ b/src/Tools/isac/ProgLang/Auto_Prog.thy	Wed Mar 18 15:23:15 2020 +0100
     5.3 @@ -195,12 +195,12 @@
     5.4  
     5.5  fun rules2scr_Rls thy rules =
     5.6      if contain_bdv rules
     5.7 -    then FunID_Term_Bdv $ (Repeat $ (((#> o (map (rule2stac_inst thy))) rules) $ Rule.e_term))
     5.8 -    else FunID_Term $ (Repeat $ (((#> o (map (rule2stac thy))) rules) $ Rule.e_term));
     5.9 +    then FunID_Term_Bdv $ (Repeat $ (((op #> o (map (rule2stac_inst thy))) rules) $ Rule.e_term))
    5.10 +    else FunID_Term $ (Repeat $ (((op #> o (map (rule2stac thy))) rules) $ Rule.e_term));
    5.11  fun rules2scr_Seq thy rules =
    5.12      if contain_bdv rules
    5.13 -    then FunID_Term_Bdv $ (((#> o (map (rule2stac_inst thy))) rules) $ Rule.e_term)
    5.14 -    else FunID_Term $ (((#> o (map (rule2stac thy))) rules) $ Rule.e_term);
    5.15 +    then FunID_Term_Bdv $ (((op #> o (map (rule2stac_inst thy))) rules) $ Rule.e_term)
    5.16 +    else FunID_Term $ (((op #> o (map (rule2stac thy))) rules) $ Rule.e_term);
    5.17  
    5.18  (* REPLACED BY Auto_Prog.gen:
    5.19     prepare the input for an rls for use:
    5.20 @@ -230,6 +230,7 @@
    5.21  
    5.22  (* on the fly generate a Prog from an rls for Math_Engine.detailstep.
    5.23    Types are not precise, but these are not required by LI.
    5.24 +  Argument "thy" is only required for lookup in KEStore.
    5.25  *)
    5.26  fun gen thy t rls =
    5.27    let

     6.1 --- a/src/Tools/isac/TODO.thy	Wed Mar 18 14:51:58 2020 +0100
     6.2 +++ b/src/Tools/isac/TODO.thy	Wed Mar 18 15:23:15 2020 +0100
     6.3 @@ -449,7 +449,6 @@
     6.4  remove Rfuns -> Rule.Prog, Rule.EmptyScr
     6.5  consider separating spec.funs. to ?Inter_Steps?
     6.6    \begin{itemize}
     6.7 -  \item removing from_pblobj_or_detail' causes many strange errors
     6.8    \item ^^^+ see from_pblobj_or_detail_thm, from_pblobj_or_detail_calc, ...
     6.9    \item xxx
    6.10    \item probably only "normal_form" seems to be needed

     7.1 --- a/test/Tools/isac/BridgeLibisabelle/use-cases.sml	Wed Mar 18 14:51:58 2020 +0100
     7.2 +++ b/test/Tools/isac/BridgeLibisabelle/use-cases.sml	Wed Mar 18 15:23:15 2020 +0100
     7.3 @@ -197,7 +197,7 @@
     7.4  "~~~~~ fun by_tactic , args:"; val (m, (pt, po as (p, p_))) = (m, (pt, p));
     7.5      (*if*) Celem.e_metID = get_obj g_metID pt (par_pblobj pt p); (*else*)
     7.6  	      val thy' = get_obj g_domID pt (par_pblobj pt p);
     7.7 -	      val (srls, is, sc) = LItool.from_pblobj_or_detail' thy' (p,p_) pt;
     7.8 +	      val (is, sc) = LItool.resume_prog thy' (p,p_) pt;
     7.9          val Safe_Step (istate, _, tac) =
    7.10            (*case*) LI.locate_input_tactic sc (pt, po) (fst is) (snd is) m (*of*);
    7.11  

     8.1 --- a/test/Tools/isac/Interpret/lucas-interpreter.sml	Wed Mar 18 14:51:58 2020 +0100
     8.2 +++ b/test/Tools/isac/Interpret/lucas-interpreter.sml	Wed Mar 18 15:23:15 2020 +0100
     8.3 @@ -119,7 +119,7 @@
     8.4  (*+*)val (pt'''''_', (p'''''_', p_'''''_')) = (pt, (p, p_));
     8.5      (*if*) Celem.e_metID = get_obj g_metID pt (par_pblobj pt p); (*else*)
     8.6  	      val thy' = get_obj g_domID pt (par_pblobj pt p);
     8.7 -	      val (_, is, sc) = LItool.from_pblobj_or_detail' thy' (p,p_) pt;
     8.8 +	      val (is, sc) = LItool.resume_prog thy' (p,p_) pt;
     8.9  
    8.10       locate_input_tactic sc (pt, po) (fst is) (snd is) m;
    8.11  "~~~~~ fun locate_input_tactic , args:"; val (Prog prog, cstate, istate, ctxt, tac)
    8.12 @@ -273,7 +273,7 @@
    8.13  "~~~~~ fun by_tactic , args:"; val (m, (pt, po as (p, p_))) = (m, (pt, p));
    8.14      (*if*) Celem.e_metID = get_obj g_metID pt (par_pblobj pt p) (*else*);
    8.15  	      val thy' = get_obj g_domID pt (par_pblobj pt p);
    8.16 -	      val (_, is, sc) = LItool.from_pblobj_or_detail' thy' (p,p_) pt;
    8.17 +	      val (is, sc) = LItool.resume_prog thy' (p,p_) pt;
    8.18  
    8.19    (*case*) locate_input_tactic sc (pt, po) (fst is) (snd is) m (*of*);
    8.20  "~~~~~ fun locate_input_tactic , args:"; val ((Rule.Prog prog), (cstate as (pt, (*?*)pos(*?*))), istate, ctxt, tac)
    8.21 @@ -369,7 +369,7 @@
    8.22  "~~~~~ and do_next , args:"; val (ptp as (pt, pos as (p, p_))) =  (pt, ip);
    8.23      (*if*) Celem.e_metID = get_obj g_metID pt (par_pblobj pt p) (*else*);
    8.24          val thy' = get_obj g_domID pt (par_pblobj pt p);
    8.25 -	      val (_, (ist, ctxt), sc) = LItool.from_pblobj_or_detail' thy' (p,p_) pt;
    8.26 +	      val ((ist, ctxt), sc) = LItool.resume_prog thy' (p,p_) pt;
    8.27  
    8.28  val Next_Step (_, _, Rewrite_Set' ("Poly", _, Seq {id = "norm_Poly", ...}, _, _)) =
    8.29             LI.find_next_step sc (pt, pos) ist ctxt (*of*);
    8.30 @@ -421,7 +421,7 @@
    8.31  "~~~~~ and do_next , args:"; val (ptp as (pt, pos as (p, p_))) =  (pt, ip);
    8.32      (*if*) Celem.e_metID = get_obj g_metID pt (par_pblobj pt p) (*else*);
    8.33          val thy' = get_obj g_domID pt (par_pblobj pt p);
    8.34 -	      val (_, (ist, ctxt), sc) = LItool.from_pblobj_or_detail' thy' (p,p_) pt;
    8.35 +	      val ((ist, ctxt), sc) = LItool.resume_prog thy' (p,p_) pt;
    8.36  
    8.37    (** )val End_Program (ist, tac) = 
    8.38   ( *case*) LI.find_next_step sc (pt, pos) ist ctxt (*of*);

     9.1 --- a/test/Tools/isac/Knowledge/polyeq-1.sml	Wed Mar 18 14:51:58 2020 +0100
     9.2 +++ b/test/Tools/isac/Knowledge/polyeq-1.sml	Wed Mar 18 15:23:15 2020 +0100
     9.3 @@ -205,7 +205,7 @@
     9.4  "~~~~~ fun Step_Solve.by_tactic , args:"; val (m, (pt, po as (p,p_))) = (m, (pt, pos));
     9.5  e_metID = get_obj g_metID pt (par_pblobj pt p) (*false*);
     9.6          val thy' = get_obj g_domID pt (par_pblobj pt p);
     9.7 -	        val (srls, is, sc) = from_pblobj_or_detail' thy' (p,p_) pt;
     9.8 +	        val (is, sc) = resume_prog thy' (p,p_) pt;
     9.9  		        val d = e_rls;
    9.10  (*locate_input_tactic (thy',srls) m  (pt,(p,p_)) (sc,d) is;
    9.11    WAS: not-found-in-script: NotLocatable from Term_Val1 (Const ("List...*)

    10.1 --- a/test/Tools/isac/Knowledge/rateq.sml	Wed Mar 18 14:51:58 2020 +0100
    10.2 +++ b/test/Tools/isac/Knowledge/rateq.sml	Wed Mar 18 15:23:15 2020 +0100
    10.3 @@ -102,7 +102,7 @@
    10.4  member op = [Pbl,Met] p_ andalso is_none (get_obj g_env pt (fst p)); (*= false*)
    10.5  "~~~~~ fun do_next, args:"; val (ptp as (pt, pos as (p, p_))) = (pt, ip);
    10.6  val thy' = get_obj g_domID pt (par_pblobj pt p);
    10.7 -val (srls, is, sc) = from_pblobj_or_detail' thy' (p,p_) pt; (*is: which ctxt?*)
    10.8 +val (is, sc) = resume_prog thy' (p,p_) pt; (*is: which ctxt?*)
    10.9  "~~~~~ fun find_next_step, args:"; val () = ();
   10.10  (*----- outcommented during cleanup of args in lucas-interpreter.sml ------------------------\\* )
   10.11  "~~~~~ fun go_scan_up, args:"; val (thy, ptp, (Prog sc), E, l, ay, a, v) =
   10.12 @@ -288,7 +288,7 @@
   10.13  "~~~~~ and do_next, args:"; val ((ptp as (pt, pos as (p,p_)))) = ((pt,ip));
   10.14  e_metID = get_obj g_metID pt (par_pblobj pt p); (* = false*)
   10.15            val thy' = get_obj g_domID pt (par_pblobj pt p);
   10.16 -	        val (srls, is, sc) = from_pblobj_or_detail' thy' (p,p_) pt;
   10.17 +	        val (is, sc) = resume_prog thy' (p,p_) pt;
   10.18  "~~~~~ fun find_next_step, args:"; val (thy, (ptp as (pt, pos as (p, _)):ctree * pos'),
   10.19    (sc as Prog (h $ body)), (Pstate (E,l,a,v,s,b), ctxt)) = ((thy',srls), (pt,pos), sc, is);
   10.20  (*----- outcommented during cleanup of args in lucas-interpreter.sml ------------------------\\* )

    11.1 --- a/test/Tools/isac/Knowledge/rootrateq.sml	Wed Mar 18 14:51:58 2020 +0100
    11.2 +++ b/test/Tools/isac/Knowledge/rootrateq.sml	Wed Mar 18 15:23:15 2020 +0100
    11.3 @@ -340,8 +340,8 @@
    11.4          val thy' = get_obj g_domID pt (par_pblobj pt p);
    11.5  
    11.6  	      val (_, (ist, ctxt), sc) =
    11.7 -    LItool.from_pblobj_or_detail' thy' (p,p_) pt;
    11.8 -"~~~~~ fun from_pblobj_or_detail' , args:"; val (thy, (p, p_), pt) = (thy', (p,p_), pt);
    11.9 +    LItool.resume_prog thy' (p,p_) pt;
   11.10 +"~~~~~ fun resume_prog , args:"; val (thy, (p, p_), pt) = (thy', (p,p_), pt);
   11.11    (*if*) Pos.on_specification p_ (*else*);
   11.12      val (pbl, p', rls') = par_pbl_det pt p
   11.13      (*if*) pbl (*then*);

    12.1 --- a/test/Tools/isac/MathEngine/mathengine-stateless.sml	Wed Mar 18 14:51:58 2020 +0100
    12.2 +++ b/test/Tools/isac/MathEngine/mathengine-stateless.sml	Wed Mar 18 15:23:15 2020 +0100
    12.3 @@ -364,7 +364,7 @@
    12.4  "~~~~~ fun do_next, args:"; val (ptp as (pt, pos as (p,p_))) = (pt,ip);
    12.5  e_metID = get_obj g_metID pt (par_pblobj pt p); (*false*)
    12.6  val thy' = get_obj g_domID pt (par_pblobj pt p);
    12.7 -val (srls, (ist, ctxt), sc) = from_pblobj_or_detail' thy' (p,p_) pt;
    12.8 +val ((ist, ctxt), sc) = resume_prog thy' (p,p_) pt;
    12.9  val Next_Step (istate, ctxt, tac) = LI.find_next_step sc (pt,pos) ist ctxt; (*WAS Empty_Tac_: tac_*)
   12.10  case tac of Or_to_List' _ => ()
   12.11  | _ => error "Or_to_List broken ?"
   12.12 @@ -467,7 +467,7 @@
   12.13  "~~~~~ fun do_next , args:"; val ((ptp as (pt, pos as (p,p_)))) = (ptp);
   12.14  e_metID = get_obj g_metID pt (par_pblobj pt p) = false;
   12.15            val thy' = get_obj g_domID pt (par_pblobj pt p);
   12.16 -	        val (srls, (ist, ctxt), sc) = from_pblobj_or_detail' thy' (p,p_) pt;
   12.17 +	        val ((ist, ctxt), sc) = resume_prog thy' (p,p_) pt;
   12.18  	        val Next_Step (is, ctxt, tac_) = LI.find_next_step sc (pt,pos) ist ctxt;
   12.19  (*tac_ = Rewrite' (..., ("rnorm_equation_add", "Test.rnorm_equation_add"), ...) !!!!!!!!!!!!!!!!*)
   12.20  

    13.1 --- a/test/Tools/isac/Minisubpbl/200-start-method.sml	Wed Mar 18 14:51:58 2020 +0100
    13.2 +++ b/test/Tools/isac/Minisubpbl/200-start-method.sml	Wed Mar 18 15:23:15 2020 +0100
    13.3 @@ -127,7 +127,7 @@
    13.4  "~~~~~ and do_next , args:"; val (ptp as (pt, pos as (p, p_))) = (pt,ip);
    13.5  Celem.e_metID = get_obj g_metID pt (par_pblobj pt p) (* = false*);
    13.6          val thy' = get_obj g_domID pt (par_pblobj pt p);
    13.7 -	      val (srls, is, sc) = LItool.from_pblobj_or_detail' thy' (p,p_) pt;
    13.8 +	      val (is, sc) = LItool.resume_prog thy' (p,p_) pt;
    13.9  "~~~~~ fun find_next_step , args:"; val ((ptp as(pt, (p, _))), (Rule.Prog prog), (Istate.Pstate ist, ctxt))
   13.10    = ((pt, pos), sc, is);
   13.11        (*case*) scan_to_tactic (prog, (ptp, ctxt)) (Istate.Pstate ist) (*of*);

    14.1 --- a/test/Tools/isac/Minisubpbl/250-Rewrite_Set-from-method.sml	Wed Mar 18 14:51:58 2020 +0100
    14.2 +++ b/test/Tools/isac/Minisubpbl/250-Rewrite_Set-from-method.sml	Wed Mar 18 15:23:15 2020 +0100
    14.3 @@ -43,7 +43,7 @@
    14.4  "~~~~~ fun by_tactic , args:"; val (m, (pt, po as (p, p_))) = (m, (pt, pos));
    14.5    (*if*) Celem.e_metID = get_obj g_metID pt (par_pblobj pt p) (* = else*);
    14.6  	      val thy' = get_obj g_domID pt (par_pblobj pt p);
    14.7 -	      val (_, is, sc) = LItool.from_pblobj_or_detail' thy' (p,p_) pt;
    14.8 +	      val (is, sc) = LItool.resume_prog thy' (p,p_) pt;
    14.9  
   14.10    val Safe_Step (_, _, Rewrite_Set' (_, _, Rls {id = "norm_equation", ...}, _, _)) = (*case*)
   14.11            locate_input_tactic sc (pt, po) (fst is) (snd is) m  (*of*);
   14.12 @@ -99,7 +99,7 @@
   14.13     e_metID = get_obj g_metID pt (par_pblobj pt p) = false;
   14.14      (*if*) Celem.e_metID = get_obj g_metID pt (par_pblobj pt p)(*else*);
   14.15          val thy' = get_obj g_domID pt (par_pblobj pt p);
   14.16 -	      val (_, (ist, ctxt), sc) = LItool.from_pblobj_or_detail' thy' (p,p_) pt;
   14.17 +	      val ((ist, ctxt), sc) = LItool.resume_prog thy' (p,p_) pt;
   14.18  
   14.19  	      val Next_Step (_, _, _) =
   14.20             (*case*)  LI.find_next_step sc (pt, pos) ist ctxt (*of*);
   14.21 @@ -153,7 +153,7 @@
   14.22  "~~~~~ and do_next , args:"; val (ptp as (pt, pos as (p, p_))) = (pt, ip);
   14.23      (*if*) Celem.e_metID = get_obj g_metID pt (par_pblobj pt p) (*else*);
   14.24          val thy' = get_obj g_domID pt (par_pblobj pt p);
   14.25 -	      val (srls, (ist, ctxt), sc) = LItool.from_pblobj_or_detail' thy' (p,p_) pt;
   14.26 +	      val ((ist, ctxt), sc) = LItool.resume_prog thy' (p,p_) pt;
   14.27  
   14.28  	      val Next_Step (_, _, _) =
   14.29             (*case*)  LI.find_next_step sc (pt, pos) ist ctxt (*of*);

    15.1 --- a/test/Tools/isac/Minisubpbl/300-init-subpbl.sml	Wed Mar 18 14:51:58 2020 +0100
    15.2 +++ b/test/Tools/isac/Minisubpbl/300-init-subpbl.sml	Wed Mar 18 15:23:15 2020 +0100
    15.3 @@ -39,7 +39,7 @@
    15.4  "~~~~~ fun by_tactic , args:"; val (m, (pt, po as (p,p_))) = (m, (pt, p));
    15.5    (*if*) e_metID = get_obj g_metID pt (par_pblobj pt p) (*false*);
    15.6  	      val thy' = get_obj g_domID pt (par_pblobj pt p);
    15.7 -	      val (srls, is, sc) = from_pblobj_or_detail' thy' (p,p_) pt;
    15.8 +	      val (is, sc) = resume_prog thy' (p,p_) pt;
    15.9  
   15.10  val Safe_Step (Pstate ist''''', ctxt''''', tac'_''''') =
   15.11             locate_input_tactic sc (pt, po) (fst is) (snd is) m;

    16.1 --- a/test/Tools/isac/Minisubpbl/400-start-meth-subpbl.sml	Wed Mar 18 14:51:58 2020 +0100
    16.2 +++ b/test/Tools/isac/Minisubpbl/400-start-meth-subpbl.sml	Wed Mar 18 15:23:15 2020 +0100
    16.3 @@ -71,7 +71,7 @@
    16.4  
    16.5  "~~~~~ and do_next , args:"; val (ptp as (pt, pos as (p, p_))) = (pt, ip);
    16.6  val thy' = get_obj g_domID pt (par_pblobj pt p);
    16.7 -val (srls, is, sc) = from_pblobj_or_detail' thy' (p,p_) pt;
    16.8 +val (is, sc) = resume_prog thy' (p,p_) pt;
    16.9  
   16.10  "~~~~~ fun find_next_step , args:"; val ((thy, _), (ptp as (pt, (p, _))), sc, (Istate.Pstate ist, _(*ctxt*)))
   16.11    = ((thy',srls), (pt,pos), sc, is);

    17.1 --- a/test/Tools/isac/Minisubpbl/470-Check_elementwise-NEXT_STEP.sml	Wed Mar 18 14:51:58 2020 +0100
    17.2 +++ b/test/Tools/isac/Minisubpbl/470-Check_elementwise-NEXT_STEP.sml	Wed Mar 18 15:23:15 2020 +0100
    17.3 @@ -54,7 +54,7 @@
    17.4  "~~~~~ and do_next , args:"; val ((ptp as (pt, pos as (p, p_)))) = ((pt, ip));
    17.5      (*if*) Celem.e_metID = get_obj g_metID pt (par_pblobj pt p) (*else*);
    17.6          val thy' = get_obj g_domID pt (par_pblobj pt p);
    17.7 -	      val (srls, (ist, ctxt), sc) = LItool.from_pblobj_or_detail' thy' (p,p_) pt;
    17.8 +	      val ((ist, ctxt), sc) = LItool.resume_prog thy' (p,p_) pt;
    17.9  
   17.10             LI.find_next_step sc (pt, pos) ist ctxt;
   17.11  "~~~~~ fun find_next_step , args:"; val (Rule.Prog prog, (ptp as(pt, (p, _))), Istate.Pstate ist, ctxt)

    18.1 --- a/test/Tools/isac/Minisubpbl/490-nxt-Check_Postcond.sml	Wed Mar 18 14:51:58 2020 +0100
    18.2 +++ b/test/Tools/isac/Minisubpbl/490-nxt-Check_Postcond.sml	Wed Mar 18 15:23:15 2020 +0100
    18.3 @@ -46,7 +46,7 @@
    18.4  "~~~~~ and do_next , args:"; val (ptp as (pt, pos as (p, p_))) = (pt, ip);
    18.5  e_metID = get_obj g_metID pt (par_pblobj pt p); (*false*)
    18.6  val thy' = get_obj g_domID pt (par_pblobj pt p);
    18.7 -val (srls, (ist, ctxt), sc) = from_pblobj_or_detail' thy' (p,p_) pt; (*is: which ctxt?*)
    18.8 +val ((ist, ctxt), sc) = resume_prog thy' (p,p_) pt; (*is: which ctxt?*)
    18.9  val End_Program (ist, tac) = LI.find_next_step sc (pt,pos) ist ctxt;
   18.10  
   18.11  (*+*);tac; (* = Check_Postcond' *)
   18.12 @@ -80,6 +80,6 @@
   18.13  val (pt,c) = append_result pt p l (scval, (*map str2term*) asm) Complete;
   18.14  (*----------------------------------------############### changed*)
   18.15  
   18.16 -val (p,_,f,nxt,_,pt) = me nxt p'''' [] pt''''; (*nxt = Check_Postcond ["LINEAR","uval (srls, is, sc) = from_pblobj_or_detail' thy' (p,p_) pt; (*is: which ctxt?*)nivariate", ...]) *);
   18.17 +val (p,_,f,nxt,_,pt) = me nxt p'''' [] pt''''; (*nxt = Check_Postcond ["LINEAR","uval (is, sc) = resume_prog thy' (p,p_) pt; (*is: which ctxt?*)nivariate", ...]) *);
   18.18  case nxt of ( Check_Postcond ["LINEAR", "univariate", "equation", "test"]) => ()
   18.19  | _ => error "450-nxt-Check_Postcond broken"

    19.1 --- a/test/Tools/isac/Minisubpbl/530-error-Check_Elementwise.sml	Wed Mar 18 14:51:58 2020 +0100
    19.2 +++ b/test/Tools/isac/Minisubpbl/530-error-Check_Elementwise.sml	Wed Mar 18 15:23:15 2020 +0100
    19.3 @@ -55,7 +55,7 @@
    19.4  "~~~~~ and do_next , args:"; val (ptp as (pt, pos as (p, p_))) = (pt, ip);
    19.5      (*if*) Celem.e_metID = get_obj g_metID pt (par_pblobj pt p) (*else*);
    19.6          val thy' = get_obj g_domID pt (par_pblobj pt p);
    19.7 -	      val (srls, (ist, ctxt), sc) = LItool.from_pblobj_or_detail' thy' (p,p_) pt;
    19.8 +	      val ((ist, ctxt), sc) = LItool.resume_prog thy' (p,p_) pt;
    19.9  
   19.10      val Next_Step (_, _, Check_elementwise' _) =
   19.11         (*case*) LI.find_next_step sc (pt, pos) ist ctxt (*of*);

    20.1 --- a/test/Tools/isac/Minisubpbl/600-postcond-NEXT_STEP.sml	Wed Mar 18 14:51:58 2020 +0100
    20.2 +++ b/test/Tools/isac/Minisubpbl/600-postcond-NEXT_STEP.sml	Wed Mar 18 15:23:15 2020 +0100
    20.3 @@ -109,7 +109,7 @@
    20.4  "~~~~~ and do_next , args:"; val (ptp as (pt, pos as (p, p_))) = (pt, ip);
    20.5      (*if*) Celem.e_metID = get_obj g_metID pt (par_pblobj pt p) (*else*);
    20.6          val thy' = get_obj g_domID pt (par_pblobj pt p);
    20.7 -	      val (_, (ist, ctxt), sc) = LItool.from_pblobj_or_detail' thy' (p,p_) pt;
    20.8 +	      val ((ist, ctxt), sc) = LItool.resume_prog thy' (p,p_) pt;
    20.9  
   20.10  (*+*)istate2str ist
   20.11   = "Pstate ([\"\n(e_e, -1 + x = 0)\",\"\n(v_v, x)\",\"\n(L_L, [x = 1])\"], [R,R,D,R,D], e_rls, NONE, \n[x = 1],"

    21.1 --- a/test/Tools/isac/Minisubpbl/700-interSteps.sml	Wed Mar 18 14:51:58 2020 +0100
    21.2 +++ b/test/Tools/isac/Minisubpbl/700-interSteps.sml	Wed Mar 18 15:23:15 2020 +0100
    21.3 @@ -117,7 +117,7 @@
    21.4  (*+*)val (keep_c', keep_ptp') = (c', ptp');
    21.5  "~~~~~ and Step_Solve.do_next , args:"; val () = ();
    21.6  (*+*)(*STOPPED HERE:
    21.7 -  NOTE: prog.xxx found by LItool.from_pblobj_or_detail' from  Rls {scr = Prog xxx, ...}*)
    21.8 +  NOTE: prog.xxx found by LItool.resume_prog from  Rls {scr = Prog xxx, ...}*)
    21.9  
   21.10  (*+*)val (c', ptp') = (keep_c', keep_ptp');
   21.11  

    22.1 --- a/test/Tools/isac/Minisubpbl/800-append-on-Frm.sml	Wed Mar 18 14:51:58 2020 +0100
    22.2 +++ b/test/Tools/isac/Minisubpbl/800-append-on-Frm.sml	Wed Mar 18 15:23:15 2020 +0100
    22.3 @@ -51,7 +51,7 @@
    22.4  "~~~~~ and do_next , args:"; val ((ptp as (pt, pos as (p, p_)))) = (pt, input_pos);
    22.5      (*if*) Celem.e_metID = get_obj g_metID pt (par_pblobj pt p) (*else*);
    22.6          val thy' = get_obj g_domID pt (par_pblobj pt p);
    22.7 -	      val (_, (ist, ctxt), sc) = LItool.from_pblobj_or_detail' thy' (p,p_) pt;
    22.8 +	      val ((ist, ctxt), sc) = LItool.resume_prog thy' (p,p_) pt;
    22.9  
   22.10  val Next_Step (ist, ctxt, tac) = (*case*)              (**..Ctree NOT updated yet**)
   22.11          LI.find_next_step sc (pt, pos) ist ctxt (*of*);

    23.1 --- a/test/Tools/isac/Test_Some.thy	Wed Mar 18 14:51:58 2020 +0100
    23.2 +++ b/test/Tools/isac/Test_Some.thy	Wed Mar 18 15:23:15 2020 +0100
    23.3 @@ -189,7 +189,7 @@
    23.4      (*if*) Celem.e_metID = get_obj g_metID pt (par_pblobj pt p) (*else*);
    23.5  \<close> ML \<open>
    23.6          val thy' = get_obj g_domID pt (par_pblobj pt p);
    23.7 -	      val (_, (ist, ctxt), sc) = LItool.from_pblobj_or_detail' thy' (p,p_) pt;
    23.8 +	      val ((ist, ctxt), sc) = LItool.resume_prog thy' (p,p_) pt;
    23.9  \<close> ML \<open>
   23.10  (*+*)Proof_Context.theory_of ctxt; (*..,Isac.RatEq}*)
   23.11  \<close> text \<open>(*Undefined fact: "all_left"*)