1.1 --- a/test/Tools/isac/Knowledge/biegelinie-3.sml	Tue Jun 25 10:46:20 2019 +0200
     1.2 +++ b/test/Tools/isac/Knowledge/biegelinie-3.sml	Tue Jun 25 12:48:24 2019 +0200
     1.3 @@ -105,13 +105,13 @@
     1.4        val ini = Lucin.init_form thy sc env;
     1.5        val p = lev_dn p;
     1.6  val NONE = (*case*) ini (*of*);
     1.7 -            val (m', (is', ctxt'), _) = next_tac (thy', srls) (pt, (p, Res)) sc (is, ctxt);
     1.8 +            val (m', (is', ctxt'), _) = determine_next_tactic (thy', srls) (pt, (p, Res)) sc (is, ctxt);
     1.9  	          val d = Rule.e_rls (*FIXME: get simplifier from domID*);
    1.10  val Steps (_, ss as (_, _, pt', p', c') :: _) =
    1.11 -(*case*) locate_gen (thy',srls) m' (pt,(p, Res)) (sc,d) (is', ctxt') (*of*);
    1.12 +(*case*) locate_input_tactic (thy',srls) m' (pt,(p, Res)) (sc,d) (is', ctxt') (*of*);
    1.13  
    1.14  (*+*)val PblObj {meth, probl, spec = (thy, _ , metID), origin = (oris, _, _), ...} = get_obj I pt' (fst p');
    1.15 -(*+*)(*MISSING after locate_gen:*)
    1.16 +(*+*)(*MISSING after locate_input_tactic:*)
    1.17  (*+*)writeln (oris2str oris); (*[
    1.18  (1, ["1"], #Given,Streckenlast, ["q_0"]),
    1.19  (2, ["1"], #Given,FunktionsVariable, ["x"]),
    1.20 @@ -120,7 +120,7 @@
    1.21                   Biegelinie
    1.22                   AbleitungBiegelinie
    1.23  *)
    1.24 -"~~~~~ fun locate_gen , args:"; val ((thy', srls), m, (pt, p),
    1.25 +"~~~~~ fun locate_input_tactic , args:"; val ((thy', srls), m, (pt, p),
    1.26  	    (scr as Rule.Prog sc, d), (Selem.ScrState (E,l,a,v,S,b), ctxt)) =
    1.27    ((thy',srls), m', (pt,(p, Res)), (sc,d), (is', ctxt'));
    1.28  val thy = Celem.assoc_thy thy';