test/Tools/isac/Knowledge/polyeq-1.sml
changeset 59845 273ffde50058
parent 59844 373d13915f8c
child 59847 566d1b41dd55
     1.1 --- a/test/Tools/isac/Knowledge/polyeq-1.sml	Tue Mar 31 15:43:33 2020 +0200
     1.2 +++ b/test/Tools/isac/Knowledge/polyeq-1.sml	Wed Apr 01 10:24:13 2020 +0200
     1.3 @@ -198,17 +198,17 @@
     1.4  (*TODO simplify assumptions (sqrt!) and check ERROR in has_degree_in*);
     1.5        (*if*) Tactic.for_specify' m; (*false*)
     1.6  (*loc_solve_ (mI,m) ptp;
     1.7 -  WAS: not-found-in-script: NotLocatable from Term_Val1 (Const ("List...*)
     1.8 +  WAS: not-found-in-program: NotLocatable from Term_Val1 (Const ("List...*)
     1.9  "~~~~~ fun loc_solve_, args:"; val (m, (pt,pos)) = (m, ptp);
    1.10  (*solve m (pt, pos);
    1.11 -  WAS: not-found-in-script: NotLocatable from Term_Val1 (Const ("List...*)
    1.12 +  WAS: not-found-in-program: NotLocatable from Term_Val1 (Const ("List...*)
    1.13  "~~~~~ fun Step_Solve.by_tactic , args:"; val (m, (pt, po as (p,p_))) = (m, (pt, pos));
    1.14  e_metID = get_obj g_metID pt (par_pblobj pt p) (*false*);
    1.15          val thy' = get_obj g_domID pt (par_pblobj pt p);
    1.16  	        val (is, sc) = resume_prog thy' (p,p_) pt;
    1.17  		        val d = e_rls;
    1.18  (*locate_input_tactic (thy',srls) m  (pt,(p,p_)) (sc,d) is;
    1.19 -  WAS: not-found-in-script: NotLocatable from Term_Val1 (Const ("List...*)
    1.20 +  WAS: not-found-in-program: NotLocatable from Term_Val1 (Const ("List...*)
    1.21  "~~~~~ fun locate_input_tactic, args:"; val () = ();
    1.22  (*----- outcommented during cleanup of args in lucas-interpreter.sml ------------------------\\* )
    1.23  l = [] orelse ((last_elem o fst) p = 0 andalso snd p = Res) (*false*);