1.1 --- a/src/Tools/isac/Interpret/lucas-interpreter.sml	Tue Nov 26 17:06:12 2019 +0100
     1.2 +++ b/src/Tools/isac/Interpret/lucas-interpreter.sml	Tue Nov 26 17:12:27 2019 +0100
     1.3 @@ -203,7 +203,11 @@
     1.4         | (form_arg, Program.Tac prog_tac) =>
     1.5             interpret_tac1 cct ist (form_arg, prog_tac)
     1.6  
     1.7 -fun scan_up1 pcct ist (Const ("Tactical.Try"(*1*), _) $ _ $ _) = go_scan_up1 pcct ist
     1.8 +fun go_scan_up1 (pcct as (prog, _)) (ist as {path, act_arg, ...}) =
     1.9 +    if 1 < length path
    1.10 +    then scan_up1 pcct (ist |> path_up) (go (path_up' path) prog)
    1.11 +    else Term_Val1 act_arg
    1.12 +and scan_up1 pcct ist (Const ("Tactical.Try"(*1*), _) $ _ $ _) = go_scan_up1 pcct ist
    1.13    | scan_up1 pcct ist (Const ("Tactical.Try"(*2*), _) $ _) = go_scan_up1 pcct ist
    1.14  
    1.15    | scan_up1 (pcct as (prog, cct as (cstate, _, _))) ist (t as Const ("Tactical.Repeat"(*1*), _) $ e $ a) =
    1.16 @@ -270,10 +274,6 @@
    1.17    | scan_up1 pcct ist (Const ("Tactical.If",_) $ _ $ _ $ _) = go_scan_up1 pcct ist
    1.18  
    1.19    | scan_up1 _ _ t = error ("scan_up1 not impl for t= " ^ Rule.term2str t)
    1.20 -and go_scan_up1 (pcct as (prog, _)) (ist as {path, act_arg, ...}) =
    1.21 -    if 1 < length path
    1.22 -    then scan_up1 pcct (ist |> path_up) (go (path_up' path) prog)
    1.23 -    else Term_Val1 act_arg
    1.24  
    1.25  fun scan_to_tactic1 (prog, (cctt as ((_, p), _, _))) (Istate.Pstate (ist as {path, ...})) =
    1.26      if path = [] orelse Pos.at_first_tactic(*RM prog path RM WITH determine_next_tactic IN solve*)p
    1.27 @@ -384,7 +384,13 @@
    1.28    	    end
    1.29  
    1.30      (*makes Reject_Tac2 to Term_Val2*)
    1.31 -fun scan_up2 pcc ist (Const ("Tactical.Try"(*1*), _) $ _ $ _) = go_scan_up2 pcc (ist |> set_appy Skip_)
    1.32 +fun go_scan_up2 (pcc as (sc, _)) (ist as {path, act_arg, finish, ...}) = 
    1.33 +    if 1 < length path
    1.34 +    then 
    1.35 +      scan_up2 pcc (ist |> path_up) (go_up path sc)
    1.36 +    else (*interpreted to end*)
    1.37 +      if finish = Skip_ then Term_Val2 act_arg else Reject_Tac2
    1.38 +and scan_up2 pcc ist (Const ("Tactical.Try"(*1*), _) $ _ $ _) = go_scan_up2 pcc (ist |> set_appy Skip_)
    1.39    | scan_up2 pcc ist (Const ("Tactical.Try"(*2*), _) $ _) = go_scan_up2 pcc (ist |> set_appy Skip_)
    1.40  
    1.41    | scan_up2 (pcc as (_, cc)) ist (Const ("Tactical.Repeat"(*1*), _) $ e $ _) =
    1.42 @@ -458,12 +464,6 @@
    1.43    | scan_up2 pcc ist (Const ("Tactical.If"(*1*), _) $ _ $ _ $ _) = go_scan_up2 pcc ist
    1.44  
    1.45    | scan_up2 _ _ t = error ("scan_up2 not impl for " ^ Rule.term2str t)
    1.46 -and go_scan_up2 (pcc as (sc, _)) (ist as {path, act_arg, finish, ...}) = 
    1.47 -    if 1 < length path
    1.48 -    then 
    1.49 -      scan_up2 pcc (ist |> path_up) (go_up path sc)
    1.50 -    else (*interpreted to end*)
    1.51 -      if finish = Skip_ then Term_Val2 act_arg else Reject_Tac2
    1.52  
    1.53  fun scan_to_tactic2 (prog, cc) (Istate.Pstate (ist as {path, ...})) =
    1.54    if path = []