1.1 --- a/src/Tools/isac/Interpret/lucas-interpreter.sml	Sat Nov 16 17:13:52 2019 +0100
     1.2 +++ b/src/Tools/isac/Interpret/lucas-interpreter.sml	Sat Nov 16 17:46:08 2019 +0100
     1.3 @@ -38,7 +38,7 @@
     1.4    datatype assoc =
     1.5        Assoc of Istate.pstate * Proof.context * Tactic.T
     1.6      | NasApp of Istate.pstate * Proof.context * Tactic.T
     1.7 -    | NasNap of  term * Env.T;
     1.8 +    | Skip1 of  term * Env.T;
     1.9    val assoc2str : assoc -> string
    1.10  (*/-------------------------------------------------------- ! aktivate for Test_Isac BEGIN ---\* )
    1.11    val go : Celem.path -> term -> term
    1.12 @@ -52,7 +52,7 @@
    1.13    val go_scan_up1: term * (Ctree.state * Proof.context * Tactic.T) -> Istate.pstate -> assoc;
    1.14    val scan_to_tactic1: term * (Ctree.state * Proof.context * Tactic.T) -> Istate.T -> assoc
    1.15  
    1.16 -  datatype appy = Appy of Tactic.T * Istate.pstate | Napp of Env.T | Skip of term * Env.T
    1.17 +  datatype appy = Appy of Tactic.T * Istate.pstate | Napp of Env.T | Skip2 of term * Env.T
    1.18    val scan_dn2: Ctree.state * Rule.theory'(*Proof.context*) -> Istate.pstate -> term -> appy
    1.19    val scan_up2: term * (Ctree.state * Rule.theory') -> Istate.pstate -> term -> appy
    1.20    val go_scan_up2: term * (Ctree.state * Rule.theory') -> Istate.pstate -> appy
    1.21 @@ -104,11 +104,11 @@
    1.22      Tactic.T        (* the Prog_Tac found as accociated to the input    *)
    1.23  | NasApp of         (* Prog_Tac is NOT associated, but applicable       *)
    1.24      Istate.pstate * Proof.context * Tactic.T
    1.25 -| NasNap of         (* Prog_Tac not associated, not applicable          *)              
    1.26 +| Skip1 of         (* Prog_Tac not associated, not applicable          *)              
    1.27  	   term *         (* in case of a Prog_Expr the respective value      *)
    1.28       Env.T;         (* *)
    1.29  fun assoc2str (Assoc _) = "Assoc"
    1.30 -  | assoc2str (NasNap _) = "NasNap"
    1.31 +  | assoc2str (Skip1 _) = "Skip1"
    1.32    | assoc2str (NasApp _) = "NasApp";
    1.33  
    1.34  
    1.35 @@ -126,7 +126,7 @@
    1.36  
    1.37    | scan_dn1 (cct as (cstate, _, _)) ist (Const ("Tactical.Chain"(*1*), _) $ e1 $ e2 $ a) =
    1.38      (case scan_dn1 cct (ist |> path_down_form ([L, L, R], a)) e1 of
    1.39 -	     NasNap (v, E)
    1.40 +	     Skip1 (v, E)
    1.41          => scan_dn1 cct (ist |> path_down [L, R] |> set_subst E (a, v)) e2
    1.42       | NasApp (ist', ctxt', tac')
    1.43         => scan_dn1 (cstate, ctxt', tac')  (ist
    1.44 @@ -134,7 +134,7 @@
    1.45       | goback => goback)
    1.46    | scan_dn1 (cct as (cstate, _, _)) ist (Const ("Tactical.Chain"(*2*), _) $e1 $ e2) =
    1.47      (case scan_dn1 cct (ist |> path_down [L, R]) e1 of
    1.48 -	     NasNap (v, E) => scan_dn1 cct (ist |> path_down [R] |> set_act_env (v, E)) e2
    1.49 +	     Skip1 (v, E) => scan_dn1 cct (ist |> path_down [R] |> set_act_env (v, E)) e2
    1.50       | NasApp (ist', ctxt', tac')
    1.51          => scan_dn1 (cstate, ctxt', tac') (ist |> path_down [R] |> trans_env_act ist') e2
    1.52       | goback => goback)
    1.53 @@ -143,7 +143,7 @@
    1.54      (case scan_dn1 cct (ist |> path_down [L, R]) e of
    1.55         NasApp (ist', _, _) =>
    1.56           scan_dn1 cct (ist' |> path_down [R, D] |> upd_env (TermC.mk_Free (id, T)) |> trans_ass ist) b
    1.57 -     | NasNap (v, E) =>
    1.58 +     | Skip1 (v, E) =>
    1.59           scan_dn1 cct (ist |> path_down [R, D] |> set_env (Env.update E (TermC.mk_Free (id, T), v))) b
    1.60       | goback => goback)
    1.61  
    1.62 @@ -151,19 +151,19 @@
    1.63      if Rewrite.eval_true_ "Isac_Knowledge" eval
    1.64        (subst_atomic (ist |> get_act_env |> Env.update' a) c)
    1.65      then scan_dn1 cct (ist |> path_down_form ([L, R], a)) e
    1.66 -    else NasNap (ist |> get_act_env)
    1.67 +    else Skip1 (ist |> get_act_env)
    1.68    | scan_dn1 cct (ist as {eval, ...}) (Const ("Tactical.While"(*2*),_) $ c $ e) =
    1.69      if Rewrite.eval_true_ "Isac_Knowledge" eval (subst_atomic (Env.update_opt' (get_subst ist)) c) 
    1.70      then scan_dn1 cct (ist |> path_down [R]) e
    1.71 -    else NasNap (ist |> get_act_env)
    1.72 +    else Skip1 (ist |> get_act_env)
    1.73  
    1.74    | scan_dn1 cct (ist as {or = Aundef, ...}) (Const ("Tactical.Or"(*1*), _) $e1 $ e2 $ a) =
    1.75      (case scan_dn1 cct (ist |> path_down_form ([L, L, R], a) |> set_or AssOnly) e1 of
    1.76 -	     NasNap (v, E) =>
    1.77 +	     Skip1 (v, E) =>
    1.78  	       (case scan_dn1 cct (ist |> path_down [L, R] |> set_subst E (a, v) |> set_or AssOnly) e2 of
    1.79 -	          NasNap (v, E) => 
    1.80 +	          Skip1 (v, E) => 
    1.81  	            (case scan_dn1 cct (ist |> path_down [L, L, R] |> set_subst E (a, v) |> set_or AssGen) e1 of
    1.82 -	               NasNap (v, E) => 
    1.83 +	               Skip1 (v, E) => 
    1.84  	                 scan_dn1 cct (ist |> path_down [L, R] |> set_subst E (a, v) |> set_or AssGen) e2
    1.85  	             | goback => goback)
    1.86  	        | goback => goback)
    1.87 @@ -171,7 +171,7 @@
    1.88       | goback => goback)
    1.89    | scan_dn1 cct ist (Const ("Tactical.Or"(*2*), _) $e1 $ e2) =
    1.90      (case scan_dn1 cct (ist |> path_down [L, R]) e1 of
    1.91 -	     NasNap (v, E) => scan_dn1 cct (ist |> path_down [R] |> set_act_env (v, E)) e2
    1.92 +	     Skip1 (v, E) => scan_dn1 cct (ist |> path_down [R] |> set_act_env (v, E)) e2
    1.93       | goback => goback)
    1.94  
    1.95    | scan_dn1 cct  (ist as {eval, ...}) (Const ("Tactical.If", _) $ c $ e1 $ e2) =
    1.96 @@ -183,7 +183,7 @@
    1.97    | scan_dn1 ((pt, p), ctxt, tac) (ist as {env, eval, or, ...}) t =
    1.98      (case Lucin.handle_leaf "locate" (Context.theory_name (Rule.Isac"")) eval (get_subst ist) t of
    1.99  	     (a', Celem.Expr _) => 
   1.100 -	       (NasNap (Rewrite.eval_listexpr_ (Celem.assoc_thy "Isac_Knowledge") eval
   1.101 +	       (Skip1 (Rewrite.eval_listexpr_ (Celem.assoc_thy "Isac_Knowledge") eval
   1.102  		       (subst_atomic (Env.update_opt'' (get_act_env ist, a')) t), env))
   1.103       | (a', Celem.STac stac) =>
   1.104           (case Lucin.associate pt ctxt (tac, stac) of
   1.105 @@ -193,11 +193,11 @@
   1.106  
   1.107             | Lucin.NotAss =>
   1.108               (case or of (* switch for Tactical.Or: 1st AssOnly, 2nd AssGen *)
   1.109 -                AssOnly => (NasNap (ist |> get_act_env))
   1.110 +                AssOnly => (Skip1 (ist |> get_act_env))
   1.111                | _(*Aundef*) =>
   1.112                   case Applicable.applicable_in p pt (Lucin.stac2tac pt (Celem.assoc_thy "Isac_Knowledge") stac) of
   1.113                      Chead.Appl m' => NasApp (ist |> set_subst_false (a', Lucin.tac_2res m'), ctxt, tac)
   1.114 -                  | Chead.Notappl _ => (NasNap (ist |> get_act_env)))
   1.115 +                  | Chead.Notappl _ => (Skip1 (ist |> get_act_env)))
   1.116      ));
   1.117  
   1.118  fun scan_up1 pcct ist (Const ("Tactical.Try"(*1*), _) $ _ $ _) = go_scan_up1 pcct ist
   1.119 @@ -205,12 +205,12 @@
   1.120  
   1.121    | scan_up1 (pcct as (prog, cct as (cstate, _, _))) ist (t as Const ("Tactical.Repeat"(*1*), _) $ e $ a) =
   1.122      (case scan_dn1 cct (ist |> path_down_form ([L, R], a) |> set_or Aundef) e of 
   1.123 -      NasNap (v, E') => go_scan_up1 pcct (ist |> set_form_env (v, E') |> set_form a)
   1.124 +      Skip1 (v, E') => go_scan_up1 pcct (ist |> set_form_env (v, E') |> set_form a)
   1.125      | NasApp (ist', ctxt', tac') => scan_up1 (prog, (cstate, ctxt', tac')) ist' t
   1.126      | goback => goback)
   1.127    | scan_up1 (pcct as (prog, cct as (cstate, _, _))) ist (t as Const ("Tactical.Repeat"(*2*), _) $ e) =
   1.128      (case scan_dn1 cct (ist |> path_down [R] |> set_or Aundef) e of
   1.129 -       NasNap (v', E') => go_scan_up1 pcct (ist |> set_act_env (v', E'))
   1.130 +       Skip1 (v', E') => go_scan_up1 pcct (ist |> set_act_env (v', E'))
   1.131       | NasApp (ist', ctxt', tac') => scan_up1 (prog, (cstate, ctxt', tac')) ist' t
   1.132       | goback => goback)
   1.133  
   1.134 @@ -223,7 +223,7 @@
   1.135         val e2 = check_Seq_up ist prog
   1.136       in
   1.137         case scan_dn1 cct (ist |> path_up_down [R] |> set_or Aundef) e2 of
   1.138 -         NasNap (v, E) => go_scan_up1 pcct (ist |> path_up |> set_act_env (v, E))
   1.139 +         Skip1 (v, E) => go_scan_up1 pcct (ist |> path_up |> set_act_env (v, E))
   1.140         | NasApp (ist', ctxt', tac') => go_scan_up1 (prog, (cstate, ctxt', tac')) ist'
   1.141         | goback => goback 
   1.142       end
   1.143 @@ -234,7 +234,7 @@
   1.144      in case scan_dn1 cct (ist |> path_up_down [R, D] |> upd_env i |> set_or Aundef) body of
   1.145  	       Assoc iss => Assoc iss
   1.146  	     | NasApp (ist', ctxt', tac') => go_scan_up1 (prog, (cstate, ctxt', tac')) ist'
   1.147 -	     | NasNap (v, E) => go_scan_up1 pcct (ist |> path_up |> set_act_env (v, E)) 
   1.148 +	     | Skip1 (v, E) => go_scan_up1 pcct (ist |> path_up |> set_act_env (v, E)) 
   1.149  	  end
   1.150    | scan_up1 pcct ist (Abs(*2*) _) = go_scan_up1 pcct ist
   1.151    | scan_up1 pcct ist (Const ("HOL.Let"(*3*), _) $ _ $ (Abs _)) = go_scan_up1 pcct ist
   1.152 @@ -244,7 +244,7 @@
   1.153      if Rewrite.eval_true_ "Isac_Knowledge" eval (subst_atomic (Env.update' a (get_act_env ist)) c)
   1.154      then
   1.155        case scan_dn1 cct (ist |> path_down_form ([L, R], a) |> set_or Aundef) e of 
   1.156 -        NasNap (v, E') => go_scan_up1 pcct (ist |> set_act_env (v, E') |> set_form a)
   1.157 +        Skip1 (v, E') => go_scan_up1 pcct (ist |> set_act_env (v, E') |> set_form a)
   1.158  
   1.159        | NasApp (ist', ctxt', tac') => scan_up1 (prog, (cstate, ctxt', tac')) ist' t
   1.160        | goback => goback
   1.161 @@ -254,7 +254,7 @@
   1.162      if Rewrite.eval_true_ "Isac_Knowledge" eval (subst_atomic (Env.update_opt' (get_subst ist)) c)
   1.163      then
   1.164        case scan_dn1 cct (ist |> path_down [R] |> set_or Aundef) e of 
   1.165 -        NasNap (v, E') => go_scan_up1 pcct (ist |> set_act_env (v, E'))
   1.166 +        Skip1 (v, E') => go_scan_up1 pcct (ist |> set_act_env (v, E'))
   1.167         | NasApp (ist', ctxt', tac') => scan_up1 (prog, (cstate, ctxt', tac')) ist' t
   1.168         | goback => goback
   1.169      else go_scan_up1 pcct ist
   1.170 @@ -271,7 +271,7 @@
   1.171  and go_scan_up1 (pcct as (prog, _)) (ist as {path, ...}) =
   1.172      if 1 < length path
   1.173      then scan_up1 pcct (ist |> path_up) (go (path_up' path) prog)
   1.174 -    else (NasNap (get_act_env ist))
   1.175 +    else (Skip1 (get_act_env ist))
   1.176  
   1.177  fun scan_to_tactic1 (prog, (cctt as ((_, p), _, _))) (Istate.Pstate (ist as {path, ...})) =
   1.178      if path = [] orelse Pos.at_first_tactic(*RM prog path RM WITH determine_next_tactic IN solve*)p
   1.179 @@ -308,9 +308,9 @@
   1.180      Tactic.T *     (* tactic_associated (fun associate) with Prog_Tac  *)
   1.181      Istate.pstate  (* the current, returned for resuming execution     *)
   1.182  | Napp of        (* stac found was not applicable; 
   1.183 -	                    this mode may become Skip in Repeat, Try and Or *)
   1.184 +	                    this mode may become Skip2 in Repeat, Try and Or *)
   1.185      Env.T      (* popped while scan_up2                             *)
   1.186 -| Skip of        (* for restart after Appy, for leaving iterations,
   1.187 +| Skip2 of        (* for restart after Appy, for leaving iterations,
   1.188  	                    for passing the value of scriptexpressions,
   1.189  		                  and for finishing the script successfully       *)
   1.190      term *         (* ???*) 
   1.191 @@ -321,11 +321,11 @@
   1.192  
   1.193  fun scan_dn2 cc (ist as {act_arg, ...}) (Const ("Tactical.Try"(*1*), _) $ e $ a) =
   1.194      (case scan_dn2 cc (ist|> path_down_form ([L, R], a)) e of
   1.195 -      Napp E => (Skip (act_arg, E))
   1.196 +      Napp E => (Skip2 (act_arg, E))
   1.197      | goback => goback)
   1.198    | scan_dn2 cc (ist as {act_arg, ...}) (Const ("Tactical.Try"(*2*), _) $ e) =
   1.199      (case scan_dn2 cc (ist |> path_down [R]) e of
   1.200 -      Napp E => (Skip (act_arg, E))
   1.201 +      Napp E => (Skip2 (act_arg, E))
   1.202      | goback => goback)
   1.203  
   1.204    | scan_dn2 cc ist (Const ("Tactical.Repeat"(*1*), _) $ e $ a) = 
   1.205 @@ -335,26 +335,26 @@
   1.206  
   1.207    | scan_dn2 cc ist (Const ("Tactical.Chain"(*1*), _) $ e1 $ e2 $ a) =
   1.208      (case scan_dn2 cc (ist |> path_down_form ([L, L, R], a)) e1 of
   1.209 -	    Skip (v, E) => scan_dn2 cc (ist |> path_down_form ([L, R], a) |> set_act_env (v, E)) e2 (*UPD*)
   1.210 +	    Skip2 (v, E) => scan_dn2 cc (ist |> path_down_form ([L, R], a) |> set_act_env (v, E)) e2 (*UPD*)
   1.211      | goback => goback)
   1.212    | scan_dn2 cc ist (Const ("Tactical.Chain"(*2*), _) $ e1 $ e2) =
   1.213      (case scan_dn2 cc (ist |> path_down [L, R]) e1 of
   1.214 -	    Skip (v, E) => scan_dn2 cc (ist |> path_down [R] |> set_act_env (v, E)) e2
   1.215 +	    Skip2 (v, E) => scan_dn2 cc (ist |> path_down [R] |> set_act_env (v, E)) e2
   1.216      | goback => goback)
   1.217  
   1.218    | scan_dn2 cc ist (Const ("HOL.Let"(*1*), _) $ e $ (Abs (i, T, b))) =
   1.219       (case scan_dn2 cc (ist |> path_down [L, R]) e of
   1.220 -       Skip (res, E) => scan_dn2 cc (ist |> path_down [R, D] |> upd_env' (E , (Free (i, T), res))) b
   1.221 +       Skip2 (res, E) => scan_dn2 cc (ist |> path_down [R, D] |> upd_env' (E , (Free (i, T), res))) b
   1.222       | goback => goback)
   1.223  
   1.224    | scan_dn2 (cc as (_, ctxt)) (ist as {eval, ...}) (Const ("Tactical.While"(*1*), _) $ c $ e $ a) =
   1.225      if Rewrite.eval_true_ ctxt eval (subst_atomic (ist |> get_act_env |> Env.update' a) c)
   1.226      then scan_dn2 cc (ist |> path_down_form ([L, R], a)) e
   1.227 -    else Skip (get_act_env ist)
   1.228 +    else Skip2 (get_act_env ist)
   1.229    | scan_dn2 (cc as (_, ctxt)) (ist as {eval, ...}) (Const ("Tactical.While"(*2*), _) $ c $ e) =
   1.230      if Rewrite.eval_true_ ctxt eval (subst_atomic (Env.update_opt' (get_subst ist)) c)
   1.231      then scan_dn2 cc (ist |> path_down [R]) e
   1.232 -    else Skip (get_act_env ist)
   1.233 +    else Skip2 (get_act_env ist)
   1.234  
   1.235    |scan_dn2 cc ist (Const ("Tactical.Or"(*1*), _) $e1 $ e2 $ a) =
   1.236      (case scan_dn2 cc (ist |> path_down_form ([L, L, R], a)) e1 of
   1.237 @@ -373,7 +373,7 @@
   1.238      (*======= end of scanning tacticals, a Prog_Tac as leaf =======*)
   1.239    | scan_dn2 ((pt, p), ctxt) (ist as {env, eval, ...}) t =
   1.240      case Lucin.handle_leaf "next  " ctxt eval (get_subst ist) t of
   1.241 -	    (_, Celem.Expr s) => Skip (s, env)
   1.242 +	    (_, Celem.Expr s) => Skip2 (s, env)
   1.243      | (a', Celem.STac stac) =>
   1.244  	    let
   1.245  	      val (m, m') = Lucin.stac2tac_ pt (Celem.assoc_thy ctxt) stac
   1.246 @@ -386,7 +386,7 @@
   1.247    		    | _ => Napp env)
   1.248  	    end
   1.249  
   1.250 -    (*makes Napp to Skip*)
   1.251 +    (*makes Napp to Skip2*)
   1.252  fun scan_up2 pcc ist (Const ("Tactical.Try"(*1*), _) $ _ $ _) = go_scan_up2 pcc (ist |> set_appy Skip_)
   1.253    | scan_up2 pcc ist (Const ("Tactical.Try"(*2*), _) $ _) = go_scan_up2 pcc (ist |> set_appy Skip_)
   1.254  
   1.255 @@ -394,13 +394,13 @@
   1.256      (case scan_dn2 cc (ist |> path_down [L, R]) e of (* no appy_: there was already a stac below *)
   1.257        Appy lr => Appy lr
   1.258      | Napp E =>  go_scan_up2 pcc (ist |> set_env E |> set_appy Skip_)
   1.259 -    | Skip (v, E) =>  go_scan_up2 pcc (ist |> set_act_env (v, E) |> set_appy Skip_))
   1.260 +    | Skip2 (v, E) =>  go_scan_up2 pcc (ist |> set_act_env (v, E) |> set_appy Skip_))
   1.261      (*no appy_: there was already a stac below*)
   1.262    | scan_up2  (pcc as (_, cc)) ist (Const ("Tactical.Repeat"(*2*), _) $ e) =
   1.263      (case scan_dn2 cc (ist |> path_down [R]) e of
   1.264        Appy lr => Appy lr
   1.265      | Napp E => go_scan_up2 pcc (ist |> set_env E |> set_appy Skip_)
   1.266 -    | Skip (v, E) => go_scan_up2 pcc (ist |> set_act_env (v, E) |> set_appy Skip_))
   1.267 +    | Skip2 (v, E) => go_scan_up2 pcc (ist |> set_act_env (v, E) |> set_appy Skip_))
   1.268  
   1.269    | scan_up2 pcc ist (Const ("Tactical.Chain"(*1*), _) $ _ $ _ $ _) = go_scan_up2 pcc ist
   1.270    | scan_up2 pcc ist (Const ("Tactical.Chain"(*2*), _) $ _ $ _) = go_scan_up2 pcc ist
   1.271 @@ -414,7 +414,7 @@
   1.272          case scan_dn2 cc (ist |> path_up_down [R]) e2 of
   1.273            Appy lr => Appy lr
   1.274          | Napp E => go_scan_up2 pcc (ist |> path_up |> set_env E)
   1.275 -        | Skip (v, E) => go_scan_up2 pcc (ist |> path_up |> set_act_env (v, E) |> set_appy Skip_)
   1.276 +        | Skip2 (v, E) => go_scan_up2 pcc (ist |> path_up |> set_act_env (v, E) |> set_appy Skip_)
   1.277        end
   1.278  
   1.279    | scan_up2 (pcc as (sc, cc)) (ist as {finish, ...}) (Const ("HOL.Let"(*1*), _) $ _) =
   1.280 @@ -427,7 +427,7 @@
   1.281          case scan_dn2 cc (ist |> path_up_down [R, D] |> upd_env i) body of
   1.282  	        Appy lre => Appy lre
   1.283  	      | Napp E => go_scan_up2 pcc (ist |> path_up |> set_env E)
   1.284 -	      | Skip (v, E) => go_scan_up2 pcc (ist |> path_up |> set_act_env (v, E) |> set_appy Skip_)
   1.285 +	      | Skip2 (v, E) => go_scan_up2 pcc (ist |> path_up |> set_act_env (v, E) |> set_appy Skip_)
   1.286  	    end
   1.287    | scan_up2 pcc ist (Abs _(*2*)) =  go_scan_up2 pcc ist
   1.288    | scan_up2 pcc ist (Const ("HOL.Let"(*3*),_) $ _ $ (Abs _)) =
   1.289 @@ -440,7 +440,7 @@
   1.290        case scan_dn2 cc (ist |> path_down [L, R]) e of
   1.291    	     Appy lr => Appy lr
   1.292    	  | Napp E => go_scan_up2 pcc (ist |> set_env E |> set_appy Skip_)
   1.293 -  	  | Skip (v, E) => go_scan_up2 pcc (ist |> set_act_env (v, E) |> set_appy Skip_)
   1.294 +  	  | Skip2 (v, E) => go_scan_up2 pcc (ist |> set_act_env (v, E) |> set_appy Skip_)
   1.295      else
   1.296        go_scan_up2 pcc (ist |> set_appy Skip_)
   1.297      (*no appy_: never causes Napp - Helpless*)
   1.298 @@ -450,7 +450,7 @@
   1.299        case scan_dn2 cc (ist |> path_down [R]) e of
   1.300    	    Appy lr => Appy lr
   1.301    	  | Napp E => go_scan_up2 pcc (ist |> set_env E |> set_appy Skip_)
   1.302 -  	  | Skip (v, E) => go_scan_up2 pcc (ist |> set_act_env (v, E) |> set_appy Skip_)
   1.303 +  	  | Skip2 (v, E) => go_scan_up2 pcc (ist |> set_act_env (v, E) |> set_appy Skip_)
   1.304      else
   1.305        go_scan_up2 pcc (ist |> set_appy Skip_)
   1.306  
   1.307 @@ -466,7 +466,7 @@
   1.308      then 
   1.309        scan_up2 pcc (ist |> path_up) (go_up path sc)
   1.310      else (*interpreted to end*)
   1.311 -      if finish = Skip_ then Skip (get_act_env ist) else Napp env
   1.312 +      if finish = Skip_ then Skip2 (get_act_env ist) else Napp env
   1.313  
   1.314  fun scan_to_tactic2 (prog, cc) (Istate.Pstate (ist as {path, ...})) =
   1.315    if path = []
   1.316 @@ -477,7 +477,7 @@
   1.317  (*decide for the next applicable Prog_Tac*)
   1.318  fun determine_next_tactic (thy, _) (ptp as (pt, (p, _))) (Rule.Prog prog) (Istate.Pstate ist, _(*ctxt*)) =
   1.319     (case scan_to_tactic2 (prog, (ptp, thy)) (Istate.Pstate ist) of
   1.320 -      Skip (v, _) =>                                                        (* program finished *)
   1.321 +      Skip2 (v, _) =>                                                        (* program finished *)
   1.322          (case par_pbl_det pt p of
   1.323  	        (true, p', _) => 
   1.324  	          let

     2.1 --- a/src/Tools/isac/Interpret/script.sml	Sat Nov 16 17:13:52 2019 +0100
     2.2 +++ b/src/Tools/isac/Interpret/script.sml	Sat Nov 16 17:46:08 2019 +0100
     2.3 @@ -198,7 +198,7 @@
     2.4      Ass of
     2.5        Tactic.T        (* SubProblem gets args instantiated in associate     *)
     2.6        * term          (* for itr_arg, result in ets                         *)
     2.7 -      * Proof.context (* separate from Tactic.T like in loacte_input_tactic *)
     2.8 +      * Proof.context (* separate from Tactic.T like in locate_input_tactic *)
     2.9    | Ass_Weak of Tactic.T * term * Proof.context
    2.10    | NotAss;
    2.11  

     3.1 --- a/test/Tools/isac/Interpret/lucas-interpreter.sml	Sat Nov 16 17:13:52 2019 +0100
     3.2 +++ b/test/Tools/isac/Interpret/lucas-interpreter.sml	Sat Nov 16 17:46:08 2019 +0100
     3.3 @@ -334,7 +334,7 @@
     3.4    val Notappl "norm_equation not applicable" =    
     3.5        (*case*) Applicable.applicable_in p pt (Lucin.stac2tac pt (Celem.assoc_thy "Isac_Knowledge") stac) (*of*);
     3.6  
     3.7 -   (NasNap (ist |> get_act_env)) (* return value *);
     3.8 +   (Skip1 (ist |> get_act_env)) (* return value *);
     3.9  
    3.10  val Rewrite' ("PolyMinus", "tless_true", _, _, ("tausche_minus",_ (*"?b ist_monom \<Longrightarrow> ?a kleiner ?b \<Longrightarrow> ?b - ?a = - ?a + ?b"*)),
    3.11     t, (res, asm)) = m;

     4.1 --- a/test/Tools/isac/Knowledge/polyeq-1.sml	Sat Nov 16 17:13:52 2019 +0100
     4.2 +++ b/test/Tools/isac/Knowledge/polyeq-1.sml	Sat Nov 16 17:46:08 2019 +0100
     4.3 @@ -199,17 +199,17 @@
     4.4  (*TODO simplify assumptions (sqrt!) and check ERROR in has_degree_in*);
     4.5  member op = specsteps mI (*false*);
     4.6  (*loc_solve_ (mI,m) ptp;
     4.7 -  WAS: not-found-in-script: NotLocatable from NasNap (Const ("List...*)
     4.8 +  WAS: not-found-in-script: NotLocatable from Skip1 (Const ("List...*)
     4.9  "~~~~~ fun loc_solve_, args:"; val (m, (pt,pos)) = ((mI,m), ptp);
    4.10  (*solve m (pt, pos);
    4.11 -  WAS: not-found-in-script: NotLocatable from NasNap (Const ("List...*)
    4.12 +  WAS: not-found-in-script: NotLocatable from Skip1 (Const ("List...*)
    4.13  "~~~~~ fun solve, args:"; val ((mI,m), (pt, po as (p,p_))) = (m, (pt, pos));
    4.14  e_metID = get_obj g_metID pt (par_pblobj pt p) (*false*);
    4.15          val thy' = get_obj g_domID pt (par_pblobj pt p);
    4.16  	        val (srls, is, sc) = from_pblobj_or_detail' thy' (p,p_) pt;
    4.17  		        val d = e_rls;
    4.18  (*locate_input_tactic (thy',srls) m  (pt,(p,p_)) (sc,d) is;
    4.19 -  WAS: not-found-in-script: NotLocatable from NasNap (Const ("List...*)
    4.20 +  WAS: not-found-in-script: NotLocatable from Skip1 (Const ("List...*)
    4.21  "~~~~~ fun locate_input_tactic, args:"; val () = ();
    4.22  (*----- outcommented during cleanup of args in lucas-interpreter.sml ------------------------\\* )
    4.23  l = [] orelse ((last_elem o fst) p = 0 andalso snd p = Res) (*false*);
    4.24 @@ -221,7 +221,7 @@
    4.25  val up = drop_last l;
    4.26    term2str (go up sc);
    4.27    (go up sc);
    4.28 -(*WAS val NasNap _ = scan_up1 ys ((E,up,a,v,S,b),ss) (go up sc)
    4.29 +(*WAS val Skip1 _ = scan_up1 ys ((E,up,a,v,S,b),ss) (go up sc)
    4.30        ... ???? ... is correct*)
    4.31  "~~~~~ fun scan_up1, args:"; val ((ys as (y,ctxt,s,Prog sc,d)), (is as (E,l,a,v,S,b),ss), 
    4.32  	   (Const ("HOL.Let",_) $ _)) = (ys, ((E,up,a,v,S,b),ss:step list), (go up sc));