test/Tools/isac/Knowledge/polyeq-1.sml
changeset 59751 fa26464c66bf
parent 59749 cc3b1807f72e
child 59753 7ad0b6cfd408
     1.1 --- a/test/Tools/isac/Knowledge/polyeq-1.sml	Thu Dec 19 16:53:52 2019 +0100
     1.2 +++ b/test/Tools/isac/Knowledge/polyeq-1.sml	Thu Dec 19 17:37:25 2019 +0100
     1.3 @@ -203,7 +203,7 @@
     1.4  "~~~~~ fun loc_solve_, args:"; val (m, (pt,pos)) = (m, ptp);
     1.5  (*solve m (pt, pos);
     1.6    WAS: not-found-in-script: NotLocatable from Term_Val1 (Const ("List...*)
     1.7 -"~~~~~ fun solve, args:"; val (m, (pt, po as (p,p_))) = (m, (pt, pos));
     1.8 +"~~~~~ fun Step_Solve.by_tactic , args:"; val (m, (pt, po as (p,p_))) = (m, (pt, pos));
     1.9  e_metID = get_obj g_metID pt (par_pblobj pt p) (*false*);
    1.10          val thy' = get_obj g_domID pt (par_pblobj pt p);
    1.11  	        val (srls, is, sc) = from_pblobj_or_detail' thy' (p,p_) pt;