1.1 --- a/src/Tools/isac/Interpret/lucas-interpreter.sml	Sun Oct 09 09:01:29 2022 +0200
     1.2 +++ b/src/Tools/isac/Interpret/lucas-interpreter.sml	Wed Oct 19 10:43:04 2022 +0200
     1.3 @@ -175,15 +175,16 @@
     1.4      then scan_dn cc (ist |> path_down [L, R]) e1
     1.5      else scan_dn cc (ist |> path_down [R]) e2
     1.6  
     1.7 -  | scan_dn (cc as (_, ctxt)) (ist as {eval, ...}) t =
     1.8 +  | scan_dn (cc as (_, ctxt)) (ist as {eval, ...}) t (*fall-through*) =
     1.9      if Tactical.contained_in t
    1.10      then raise TERM ("scan_dn expects Prog_Tac or Prog_Expr", [t])
    1.11      else
    1.12        case LItool.check_leaf "next  " ctxt eval (get_subst ist) t of
    1.13    	    (Program.Expr s, _) => Term_Val s (*TODO?: include set_found here and drop those after call*)
    1.14        | (Program.Tac prog_tac, form_arg) =>
    1.15 -          check_tac cc ist (prog_tac, form_arg)
    1.16 -
    1.17 +          (tracing ("### scan_dn fall-through, prog_tac = " ^ quote (UnparseC.term prog_tac) ^ " |");
    1.18 +check_tac cc ist (prog_tac, form_arg))
    1.19 +                                       
    1.20  fun go_scan_up (pcc as (sc, _)) (ist as {path, act_arg, found_accept, ...}) = 
    1.21      if path = [R] (*root of the program body*) then
    1.22        if found_accept then