1.1 --- a/src/Tools/isac/Interpret/script.sml	Tue Jun 25 10:46:20 2019 +0200
     1.2 +++ b/src/Tools/isac/Interpret/script.sml	Tue Jun 25 12:48:24 2019 +0200
     1.3 @@ -45,7 +45,7 @@
     1.4  
     1.5  end 
     1.6  
     1.7 -(* traces the leaves (ie. non-tactical nodes) of Prog found by next_tac, see "and scr" *)   
     1.8 +(* traces the leaves (ie. non-tactical nodes) of Prog found by determine_next_tactic, see "and scr" *)   
     1.9  val trace_script = Unsynchronized.ref false; (* TODO: how are traces done in Isabelle? *)
    1.10  
    1.11  structure Lucin(**): LUCAS_INTERPRETER_DEL(**) =
    1.12 @@ -638,7 +638,7 @@
    1.13  	         val metID = get_obj g_metID pt p'
    1.14  	         val {srls,...} = Specify.get_met metID
    1.15  	       in (srls, get_loc pt (p,p_), (#scr o Specify.get_met) metID) end
    1.16 -       else (*FIXME.WN0?: get from pbl or met !!! unused for Rrls in locate_gen, next_tac*) (* 3 *)
    1.17 +       else (*FIXME.WN0?: get from pbl or met !!! unused for Rrls in locate_input_formula, determine_next_tactic*) (* 3 *)
    1.18  	       (Rule.e_rls, get_loc pt (p,p_),
    1.19  	          case rls' of
    1.20  		          Rule.Rls {scr = scr,...} => scr