1.1 --- a/TODO.md	Sat Dec 30 06:22:52 2023 +0100
     1.2 +++ b/TODO.md	Sat Dec 30 07:07:58 2023 +0100
     1.3 @@ -44,6 +44,7 @@
     1.4  * WN: cut out Calc.state_pre, Calc.state_post; only Ctree.state shall remain
     1.5    ?or could that be reasonable also together with Isabelle/PIDE?
     1.6  
     1.7 +
     1.8  ***** priority of WN items is top down, most urgent/simple on top
     1.9  
    1.10  * WN: 

     2.1 --- a/src/Tools/isac/Doc/Lucas_Interpreter/Lucas_Interpreter.thy	Sat Dec 30 06:22:52 2023 +0100
     2.2 +++ b/src/Tools/isac/Doc/Lucas_Interpreter/Lucas_Interpreter.thy	Sat Dec 30 07:07:58 2023 +0100
     2.3 @@ -506,12 +506,12 @@
     2.4  that the former requires the whole program for @{term go_scan_up} as follows:
     2.5  \<close> 
     2.6  (*<*)ML(*>*) \<open>
     2.7 -fun go_scan_up (pcc as (sc, _)) (ist as {path, act_arg, found_accept,...})=
     2.8 +fun go_scan_up (pcc as (sc, (_, ctxt))) (ist as {path, act_arg, found_accept,...})=
     2.9      if path = [R]
    2.10      then
    2.11        if found_accept then Term_Val act_arg else Reject_Tac
    2.12      else 
    2.13 -      scan_up pcc (ist |> path_up) (go_up path sc)
    2.14 +      scan_up pcc (ist |> path_up) (go_up ctxt path sc)
    2.15  and scan_up pcc ist (Const ("Tactical.Try"(*2*), _) $ _) = go_scan_up pcc ist
    2.16    | scan_up (pcc as (_, cc)) ist (Const ("Tactical.Repeat"(*2*), _) $ e) =
    2.17      (case scan_dn cc (ist |> path_down [R]) e of
    2.18 @@ -520,15 +520,14 @@
    2.19      | Term_Val v => go_scan_up pcc (ist |> set_act v |> set_found))
    2.20    | scan_up pcc ist (Const ("Tactical.Chain"(*2*), _) $ _ $ _) =
    2.21      go_scan_up pcc ist
    2.22 -  | scan_up (pcc as (sc, cc)) ist (Const ("Tactical.Chain"(*3*), _) $ _) =
    2.23 +  | scan_up (pcc as (sc, cc as (_, ctxt))) ist (Const (\<^const_name>\<open>Tactical.Chain\<close>(*3*), _) $ _) =
    2.24        let 
    2.25 -        val e2 = check_Seq_up ist sc
    2.26 +        val e2 = check_Seq_up ctxt ist sc
    2.27        in
    2.28          case scan_dn cc (ist |> path_up_down [R]) e2 of
    2.29            Accept_Tac ict => Accept_Tac ict
    2.30          | Reject_Tac => go_scan_up pcc (ist |> path_up)
    2.31 -        | Term_Val v => go_scan_up pcc (ist |> path_up |> set_act v |> 
    2.32 -set_found)
    2.33 +        | Term_Val v => go_scan_up pcc (ist |> path_up |> set_act v |> set_found)
    2.34        end
    2.35  (*|*)
    2.36  \<close>
    2.37 @@ -580,7 +579,6 @@
    2.38  
    2.39  \subsection{Guarding and Embedding Execution}\label{embedding}
    2.40  %-----------------------------------------------------------------------------
    2.41 -Guardin
    2.42  
    2.43  @{theory_text partial_function}s as used by \LI{} are alien to HOL for 
    2.44  fundamental reasons. And when the \sisac-project started with the aim to